Theorem spwpr2 8658

Description: Property of supremum defining condition for an unordered pair.

Hypothesis

Ref	Expression
spwmo.1	|- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))

Assertion

Ref	Expression
spwpr2	|- (((R e. T /\ A = {B, C}) /\ (B e. U /\ C e. W)) -> (ph <-> ((BRx /\ CRx) /\ A.y e. X ((BRy /\ CRy) -> xRy))))

Distinct variable groups:   x,y,z,A   y,B,z   y,C,z   x,R,y,z   x,X,y   y,U   y,W

Proof of Theorem spwpr2

Step	Hyp	Ref	Expression
1		raleq1 1786	. . . . 5 |- (A = {B, C} -> (A.y e. A yRx <-> A.y e. {B, C}yRx))
2		ax-17 971	. . . . . . . 8 |- (BRx -> A.y BRx)
3		breq1 2622	. . . . . . . 8 |- (y = B -> (yRx <-> BRx))
4	2, 3	ceqsalg 1825	. . . . . . 7 |- (B e. U -> (A.y(y = B -> yRx) <-> BRx))
5		ax-17 971	. . . . . . . 8 |- (CRx -> A.y CRx)
6		breq1 2622	. . . . . . . 8 |- (y = C -> (yRx <-> CRx))
7	5, 6	ceqsalg 1825	. . . . . . 7 |- (C e. W -> (A.y(y = C -> yRx) <-> CRx))
8	4, 7	bi2anan9 632	. . . . . 6 |- ((B e. U /\ C e. W) -> ((A.y(y = B -> yRx) /\ A.y(y = C -> yRx)) <-> (BRx /\ CRx)))
9		df-ral 1649	. . . . . . 7 |- (A.y e. {B, C}yRx <-> A.y(y e. {B, C} -> yRx))
10		visset 1813	. . . . . . . . . . 11 |- y e. V
11	10	elpr 2424	. . . . . . . . . 10 |- (y e. {B, C} <-> (y = B \/ y = C))
12	11	imbi1i 186	. . . . . . . . 9 |- ((y e. {B, C} -> yRx) <-> ((y = B \/ y = C) -> yRx))
13		jaob 422	. . . . . . . . 9 |- (((y = B \/ y = C) -> yRx) <-> ((y = B -> yRx) /\ (y = C -> yRx)))
14	12, 13	bitr 173	. . . . . . . 8 |- ((y e. {B, C} -> yRx) <-> ((y = B -> yRx) /\ (y = C -> yRx)))
15	14	albii 999	. . . . . . 7 |- (A.y(y e. {B, C} -> yRx) <-> A.y((y = B -> yRx) /\ (y = C -> yRx)))
16		19.26 1067	. . . . . . 7 |- (A.y((y = B -> yRx) /\ (y = C -> yRx)) <-> (A.y(y = B -> yRx) /\ A.y(y = C -> yRx)))
17	9, 15, 16	3bitr 177	. . . . . 6 |- (A.y e. {B, C}yRx <-> (A.y(y = B -> yRx) /\ A.y(y = C -> yRx)))
18	8, 17	syl5bb 532	. . . . 5 |- ((B e. U /\ C e. W) -> (A.y e. {B, C}yRx <-> (BRx /\ CRx)))
19	1, 18	sylan9bb 540	. . . 4 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> (A.y e. A yRx <-> (BRx /\ CRx)))
20		raleq1 1786	. . . . . . 7 |- (A = {B, C} -> (A.z e. A zRy <-> A.z e. {B, C}zRy))
21		ax-17 971	. . . . . . . . . 10 |- (BRy -> A.z BRy)
22		breq1 2622	. . . . . . . . . 10 |- (z = B -> (zRy <-> BRy))
23	21, 22	ceqsalg 1825	. . . . . . . . 9 |- (B e. U -> (A.z(z = B -> zRy) <-> BRy))
24		ax-17 971	. . . . . . . . . 10 |- (CRy -> A.z CRy)
25		breq1 2622	. . . . . . . . . 10 |- (z = C -> (zRy <-> CRy))
26	24, 25	ceqsalg 1825	. . . . . . . . 9 |- (C e. W -> (A.z(z = C -> zRy) <-> CRy))
27	23, 26	bi2anan9 632	. . . . . . . 8 |- ((B e. U /\ C e. W) -> ((A.z(z = B -> zRy) /\ A.z(z = C -> zRy)) <-> (BRy /\ CRy)))
28		df-ral 1649	. . . . . . . . 9 |- (A.z e. {B, C}zRy <-> A.z(z e. {B, C} -> zRy))
29		visset 1813	. . . . . . . . . . . . 13 |- z e. V
30	29	elpr 2424	. . . . . . . . . . . 12 |- (z e. {B, C} <-> (z = B \/ z = C))
31	30	imbi1i 186	. . . . . . . . . . 11 |- ((z e. {B, C} -> zRy) <-> ((z = B \/ z = C) -> zRy))
32		jaob 422	. . . . . . . . . . 11 |- (((z = B \/ z = C) -> zRy) <-> ((z = B -> zRy) /\ (z = C -> zRy)))
33	31, 32	bitr 173	. . . . . . . . . 10 |- ((z e. {B, C} -> zRy) <-> ((z = B -> zRy) /\ (z = C -> zRy)))
34	33	albii 999	. . . . . . . . 9 |- (A.z(z e. {B, C} -> zRy) <-> A.z((z = B -> zRy) /\ (z = C -> zRy)))
35		19.26 1067	. . . . . . . . 9 |- (A.z((z = B -> zRy) /\ (z = C -> zRy)) <-> (A.z(z = B -> zRy) /\ A.z(z = C -> zRy)))
36	28, 34, 35	3bitr 177	. . . . . . . 8 |- (A.z e. {B, C}zRy <-> (A.z(z = B -> zRy) /\ A.z(z = C -> zRy)))
37	27, 36	syl5bb 532	. . . . . . 7 |- ((B e. U /\ C e. W) -> (A.z e. {B, C}zRy <-> (BRy /\ CRy)))
38	20, 37	sylan9bb 540	. . . . . 6 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> (A.z e. A zRy <-> (BRy /\ CRy)))
39	38	imbi1d 613	. . . . 5 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> ((A.z e. A zRy -> xRy) <-> ((BRy /\ CRy) -> xRy)))
40	39	ralbidv 1663	. . . 4 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> (A.y e. X (A.z e. A zRy -> xRy) <-> A.y e. X ((BRy /\ CRy) -> xRy)))
41	19, 40	anbi12d 628	. . 3 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> ((BRx /\ CRx) /\ A.y e. X ((BRy /\ CRy) -> xRy))))
42	41	adantll 392	. 2 |- (((R e. T /\ A = {B, C}) /\ (B e. U /\ C e. W)) -> ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> ((BRx /\ CRx) /\ A.y e. X ((BRy /\ CRy) -> xRy))))
43		spwmo.1	. 2 |- (ph <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))
44	42, 43	syl5bb 532	1 |- (((R e. T /\ A = {B, C}) /\ (B e. U /\ C e. W)) -> (ph <-> ((BRx /\ CRx) /\ A.y e. X ((BRy /\ CRy) -> xRy))))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  A.wral 1645  {cpr 2410   class class class wbr 2619

This theorem is referenced by:  spwpr3OLD 8662  spwpr4OLD 8663  spwpr4aOLD 8664

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain