Theorem spwpr4OLD 8670

Description: Supremum of an unordered pair.

Hypothesis

Ref	Expression
spwpr4.1	|- X = dom R

Assertion

Ref	Expression
spwpr4OLD	|- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> (R supw {A, B}) = C)

Distinct variable groups:   x,A   x,B   x,C   x,R   x,X

Proof of Theorem spwpr4OLD

Step	Hyp	Ref	Expression
1		spwpr4.1	. . . 4 |- X = dom R
2		pm4.2 170	. . . 4 |- ((A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)) <-> (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)))
3	1, 2	spwval 8667	. . 3 |- ((R e. Poset /\ {A, B} e. V /\ E.y e. X (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx))) -> (R supw {A, B}) = U.{y e. X | (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx))})
4		simpll 414	. . . 4 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC)) -> R e. Poset)
5	4	3adant3 803	. . 3 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> R e. Poset)
6		prex 2795	. . . 4 |- {A, B} e. V
7	6	a1i 8	. . 3 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> {A, B} e. V)
8		breq2 2636	. . . . . . . . 9 |- (y = C -> (ARy <-> ARC))
9		breq2 2636	. . . . . . . . 9 |- (y = C -> (BRy <-> BRC))
10	8, 9	anbi12d 631	. . . . . . . 8 |- (y = C -> ((ARy /\ BRy) <-> (ARC /\ BRC)))
11		breq1 2635	. . . . . . . . . 10 |- (y = C -> (yRx <-> CRx))
12	11	imbi2d 615	. . . . . . . . 9 |- (y = C -> (((ARx /\ BRx) -> yRx) <-> ((ARx /\ BRx) -> CRx)))
13	12	ralbidv 1670	. . . . . . . 8 |- (y = C -> (A.x e. X ((ARx /\ BRx) -> yRx) <-> A.x e. X ((ARx /\ BRx) -> CRx)))
14	10, 13	anbi12d 631	. . . . . . 7 |- (y = C -> (((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx)) <-> ((ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx))))
15	14	rcla4ev 1884	. . . . . 6 |- ((C e. X /\ ((ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx))) -> E.y e. X ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx)))
16	15	3impb 833	. . . . 5 |- ((C e. X /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> E.y e. X ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx)))
17	16	3adant1l 856	. . . 4 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> E.y e. X ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx)))
18		eqid 1482	. . . . . . . 8 |- {A, B} = {A, B}
19	2	spwpr2 8666	. . . . . . . 8 |- (((R e. Poset /\ {A, B} = {A, B}) /\ (A e. V /\ B e. V)) -> ((A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)) <-> ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))))
20	18, 19	mpanl2 711	. . . . . . 7 |- ((R e. Poset /\ (A e. V /\ B e. V)) -> ((A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)) <-> ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))))
21		psrel 8654	. . . . . . . . . 10 |- (R e. Poset -> Rel R)
22		brrelex 3221	. . . . . . . . . . . 12 |- ((Rel R /\ ARC) -> A e. V)
23	22	ex 373	. . . . . . . . . . 11 |- (Rel R -> (ARC -> A e. V))
24		brrelex 3221	. . . . . . . . . . . 12 |- ((Rel R /\ BRC) -> B e. V)
25	24	ex 373	. . . . . . . . . . 11 |- (Rel R -> (BRC -> B e. V))
26	23, 25	anim12d 561	. . . . . . . . . 10 |- (Rel R -> ((ARC /\ BRC) -> (A e. V /\ B e. V)))
27	21, 26	syl 10	. . . . . . . . 9 |- (R e. Poset -> ((ARC /\ BRC) -> (A e. V /\ B e. V)))
28	27	imp 350	. . . . . . . 8 |- ((R e. Poset /\ (ARC /\ BRC)) -> (A e. V /\ B e. V))
29	28	adantlr 395	. . . . . . 7 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC)) -> (A e. V /\ B e. V))
30	20, 4, 29	sylanc 474	. . . . . 6 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC)) -> ((A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)) <-> ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))))
31	30	rexbidv 1671	. . . . 5 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC)) -> (E.y e. X (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)) <-> E.y e. X ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))))
32	31	3adant3 803	. . . 4 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> (E.y e. X (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)) <-> E.y e. X ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))))
33	17, 32	mpbird 196	. . 3 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> E.y e. X (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx)))
34	3, 5, 7, 33	syl3anc 862	. 2 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> (R supw {A, B}) = U.{y e. X | (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx))})
35	30	rabbisdv 1814	. . . 4 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC)) -> {y e. X | (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx))} = {y e. X | ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))})
36	35	unieqd 2524	. . 3 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC)) -> U.{y e. X | (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx))} = U.{y e. X | ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))})
37	36	3adant3 803	. 2 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx)) -> U.{y e. X | (A.x e. {A, B}xRy /\ A.x e. X (A.z e. {A, B}zRx -> yRx))} = U.{y e. X | ((ARy /\ BRy) /\ A.x e. X ((ARx /\ BRx) -> yRx))})
38		3simpc 791	. . 3 |- (((R e. Poset /\ C e. X) /\ (ARC /\ BRC) /\ A.x e. X ((ARx /\ BRx) -> CRx))