Theorem spwpr2 8654

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 1789	. . . . 5 |- (A = {B, C} -> (A.y e. A yRx <-> A.y e. {B, C}yRx))
2		ax-17 973	. . . . . . . 8 |- (BRx -> A.y BRx)
3		breq1 2627	. . . . . . . 8 |- (y = B -> (yRx <-> BRx))
4	2, 3	ceqsalg 1828	. . . . . . 7 |- (B e. U -> (A.y(y = B -> yRx) <-> BRx))
5		ax-17 973	. . . . . . . 8 |- (CRx -> A.y CRx)
6		breq1 2627	. . . . . . . 8 |- (y = C -> (yRx <-> CRx))
7	5, 6	ceqsalg 1828	. . . . . . 7 |- (C e. W -> (A.y(y = C -> yRx) <-> CRx))
8	4, 7	bi2anan9 634	. . . . . 6 |- ((B e. U /\ C e. W) -> ((A.y(y = B -> yRx) /\ A.y(y = C -> yRx)) <-> (BRx /\ CRx)))
9		df-ral 1652	. . . . . . 7 |- (A.y e. {B, C}yRx <-> A.y(y e. {B, C} -> yRx))
10		visset 1816	. . . . . . . . . . 11 |- y e. V
11	10	elpr 2428	. . . . . . . . . 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 424	. . . . . . . . 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 1001	. . . . . . 7 |- (A.y(y e. {B, C} -> yRx) <-> A.y((y = B -> yRx) /\ (y = C -> yRx)))
16		19.26 1069	. . . . . . 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 534	. . . . 5 |- ((B e. U /\ C e. W) -> (A.y e. {B, C}yRx <-> (BRx /\ CRx)))
19	1, 18	sylan9bb 542	. . . 4 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> (A.y e. A yRx <-> (BRx /\ CRx)))
20		raleq1 1789	. . . . . . 7 |- (A = {B, C} -> (A.z e. A zRy <-> A.z e. {B, C}zRy))
21		ax-17 973	. . . . . . . . . 10 |- (BRy -> A.z BRy)
22		breq1 2627	. . . . . . . . . 10 |- (z = B -> (zRy <-> BRy))
23	21, 22	ceqsalg 1828	. . . . . . . . 9 |- (B e. U -> (A.z(z = B -> zRy) <-> BRy))
24		ax-17 973	. . . . . . . . . 10 |- (CRy -> A.z CRy)
25		breq1 2627	. . . . . . . . . 10 |- (z = C -> (zRy <-> CRy))
26	24, 25	ceqsalg 1828	. . . . . . . . 9 |- (C e. W -> (A.z(z = C -> zRy) <-> CRy))
27	23, 26	bi2anan9 634	. . . . . . . 8 |- ((B e. U /\ C e. W) -> ((A.z(z = B -> zRy) /\ A.z(z = C -> zRy)) <-> (BRy /\ CRy)))
28		df-ral 1652	. . . . . . . . 9 |- (A.z e. {B, C}zRy <-> A.z(z e. {B, C} -> zRy))
29		visset 1816	. . . . . . . . . . . . 13 |- z e. V
30	29	elpr 2428	. . . . . . . . . . . 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 424	. . . . . . . . . . 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 1001	. . . . . . . . 9 |- (A.z(z e. {B, C} -> zRy) <-> A.z((z = B -> zRy) /\ (z = C -> zRy)))
35		19.26 1069	. . . . . . . . 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 534	. . . . . . 7 |- ((B e. U /\ C e. W) -> (A.z e. {B, C}zRy <-> (BRy /\ CRy)))
38	20, 37	sylan9bb 542	. . . . . 6 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> (A.z e. A zRy <-> (BRy /\ CRy)))
39	38	imbi1d 615	. . . . 5 |- ((A = {B, C} /\ (B e. U /\ C e. W)) -> ((A.z e. A zRy -> xRy) <-> ((BRy /\ CRy) -> xRy)))
40	39	ralbidv 1666	. . . 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 630	. . 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 394	. 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 534	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 956   = wceq 958   e. wcel 960  A.wral 1648  {cpr 2414   class class class wbr 2624

This theorem is referenced by:  spwpr4OLD 8658  spwpr4aOLD 8659

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-ral 1652  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain