Theorem supdef 14604

Description: If it exists, a supremum of A is greater or equal to every element of A and is the least upper bound of A. Here the existence of the supremum is expressed by the idiom (R sup_w A) e. X.

Hypothesis

Ref	Expression
supdef.1	|- X = dom R

Assertion

Ref	Expression
supdef	|- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))

Distinct variable groups:   y,A,z   y,R,z   y,X

Proof of Theorem supdef

Step	Hyp	Ref	Expression
1		supdef.1	. . . 4 |- X = dom R
2		biid 187	. . . 4 |- ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))
3	1, 2	spwex 10005	. . 3 |- ((R e. Poset /\ A e. W) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> (R supw A) e. X))
4	3	biimp3ar 1195	. 2 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))
5	2	spweu 10000	. . . . . . 7 |- ((R e. Poset /\ E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) -> E!x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)))
6	5	ex 402	. . . . . 6 |- (R e. Poset -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> E!x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))))
7		psdmrn 9991	. . . . . . . . . . . . . 14 |- (R e. Poset -> (dom R = U.U.R /\ ran R = U.U.R))
8		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X = U.U.R -> (x e. X <-> x e. U.U.R))
9		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (X = U.U.R -> (y e. X <-> y e. U.U.R))
10	9	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (X = U.U.R -> ((y e. X -> (A.z e. A zRy -> xRy)) <-> (y e. U.U.R -> (A.z e. A zRy -> xRy))))
11	10	ralbidv2 2125	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X = U.U.R -> (A.y e. X (A.z e. A zRy -> xRy) <-> A.y e. U.U.R(A.z e. A zRy -> xRy)))
12	11	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X = U.U.R -> ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))))
13	8, 12	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . 22 |- (X = U.U.R -> ((x e. X /\ (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))) <-> (x e. U.U.R /\ (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy)))))
14	13	rexbidv2 2126	. . . . . . . . . . . . . . . . . . . . 21 |- (X = U.U.R -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> E.x e. U.U.R(A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))))
15		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((X = dom R /\ dom R = U.U.R) -> X = U.U.R)
16		rabeq 2289	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (U.U.R = X -> {x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} = {x e. X | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))})
17	16	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (X = U.U.R -> {x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} = {x e. X | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))})
18		eqcom 1886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (X = U.U.R <-> U.U.R = X)
19	18	biimpi 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (X = U.U.R -> U.U.R = X)
20		biidd 188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (X = U.U.R -> ((A.z e. A zRy -> xRy) <-> (A.z e. A zRy -> xRy)))
21	19, 20	raleqbidv 2274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (X = U.U.R -> (A.y e. U.U.R(A.z e. A zRy -> xRy) <-> A.y e. X (A.z e. A zRy -> xRy)))
22	21	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (X = U.U.R -> ((A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy)) <-> (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))))
23	22	rabbidv 2287	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (X = U.U.R -> {x e. X | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} = {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))})
24	17, 23	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (X = U.U.R -> {x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} = {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))})
25	24	unieqd 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (X = U.U.R -> U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} = U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))})
26	25	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (X = U.U.R -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} <-> (R supw A) = U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}))
27		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} = (R supw A) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} <-> (R supw A) e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}))
28	27	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} = (R supw A) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (R supw A) e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}))
29	28	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((R supw A) = U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (R supw A) e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))}))
30		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = (R supw A) -> (yRx <-> yR(R supw A)))
31	30	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = (R supw A) -> (A.y e. A yRx <-> A.y e. A yR(R supw A)))
32		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (x = (R supw A) -> (xRy <-> (R supw A)Ry))
33	32	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (x = (R supw A) -> ((A.z e. A zRy -> xRy) <-> (A.z e. A zRy -> (R supw A)Ry)))
34	33	ralbidv 2123	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (x = (R supw A) -> (A.y e. X (A.z e. A zRy -> xRy) <-> A.y e. X (A.z e. A zRy -> (R supw A)Ry)))
35	31, 34	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (x = (R supw A) -> ((A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) <-> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
36	35	elrab3 2415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((R supw A) e. X -> ((R supw A) e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} <-> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
37	36	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((R supw A) e. X -> ((R supw A) e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
38	37	3ad2ant3 899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
39	29, 38	syl9 71	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((R supw A) = U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
40	26, 39	syl6bi 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (X = U.U.R -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
41	40	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (X = U.U.R -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
42	15, 41	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((X = dom R /\ dom R = U.U.R) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
43	1, 42	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (dom R = U.U.R -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
44	43	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((dom R = U.U.R /\ ran R = U.U.R) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
45	7, 44	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (R e. Poset -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
46	45	3ad2ant1 897	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
47	46	pm2.43i 78	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))} -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
48		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- U.U.R = U.U.R
49		biid 187	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy)) <-> (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy)))
50	48, 49	spwval3 9997	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((R e. Poset /\ A e. W /\ E.x e. U.U.R(A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))) -> (R supw A) = U.{x e. U.U.R | (A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))})
51	47, 50	syl5com 63	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. Poset /\ A e. W /\ E.x e. U.U.R(A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy))) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
52	51	3expia 1069	. . . . . . . . . . . . . . . . . . . . . 22 |- ((R e. Poset /\ A e. W) -> (E.x e. U.U.R(A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy)) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
53	52	com12 14	. . . . . . . . . . . . . . . . . . . . 21 |- (E.x e. U.U.R(A.y e. A yRx /\ A.y e. U.U.R(A.z e. A zRy -> xRy)) -> ((R e. Poset /\ A e. W) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
54	14, 53	syl6bi 231	. . . . . . . . . . . . . . . . . . . 20 |- (X = U.U.R -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> ((R e. Poset /\ A e. W) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))))
55	54	com4t 44	. . . . . . . . . . . . . . . . . . 19 |- ((R e. Poset /\ A e. W) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (X = U.U.R -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))))
56	55	3adant3 896	. . . . . . . . . . . . . . . . . 18 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (X = U.U.R -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))))
57	56	pm2.43i 78	. . . . . . . . . . . . . . . . 17 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (X = U.U.R -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
58	57, 15	syl5com 63	. . . . . . . . . . . . . . . 16 |- ((X = dom R /\ dom R = U.U.R) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
59	1, 58	mpan 759	. . . . . . . . . . . . . . 15 |- (dom R = U.U.R -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
60	59	adantr 425	. . . . . . . . . . . . . 14 |- ((dom R = U.U.R /\ ran R = U.U.R) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
61	7, 60	syl 12	. . . . . . . . . . . . 13 |- (R e. Poset -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
62	61	3ad2ant1 897	. . . . . . . . . . . 12 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
63	62	pm2.43i 78	. . . . . . . . . . 11 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
64	63	com12 14	. . . . . . . . . 10 |- (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
65	3, 64	syl6bir 232	. . . . . . . . 9 |- ((R e. Poset /\ A e. W) -> ((R supw A) e. X -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))))
66	65	3impia 1064	. . . . . . . 8 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
67	66	pm2.43i 78	. . . . . . 7 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
68		reucl2 3814	. . . . . . 7 |- (E!x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> U.{x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))} e. {x e. X | (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy))})
69	67, 68	syl5com 63	. . . . . 6 |- (E!x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
70	6, 69	syl6 25	. . . . 5 |- (R e. Poset -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
71	70	com23 36	. . . 4 |- (R e. Poset -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
72	71	3ad2ant1 897	. . 3 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))))
73	72	pm2.43i 78	. 2 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (E.x e. X (A.y e. A yRx /\ A.y e. X (A.z e. A zRy -> xRy)) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry))))
74	4, 73	mpd 29	1 |- ((R e. Poset /\ A e. W /\ (R supw A) e. X) -> (A.y e. A yR(R supw A) /\ A.y e. X (A.z e. A zRy -> (R supw A)Ry)))

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  U.cuni 3177   class class class wbr 3338  dom cdm 3986  ran crn 3987  (class class class)co 4884  Posetcps 9980   sup_w cspw 9981

This theorem is referenced by:  supdefa 14605  defge3 14613  supaub 14615  suplub2 14616  supnuf 15041

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-er 5318  df-en 5427  df-dom 5428  df-sdom 5429  df-ps 9984  df-spw 9985

Copyright terms: Public domain