Theorem zorn2lem7 4777

Description: Lemma for zorn2 4779.

Hypotheses

Ref	Expression
zorn2lem.1	|- A e. V
zorn2lem.2	|- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
zorn2lem.3	|- F = U.B
zorn2lem.4	|- C = {z e. A | A.g e. ran f gRz}
zorn2lem.5	|- D = {z e. A | A.g e. (F"x)gRz}
zorn2lem.6	|- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
zorn2lem.7	|- H = {z e. A | A.g e. (F"y)gRz}

Assertion

Ref	Expression
zorn2lem7	|- ((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> E.a e. A A.b e. A -. aRb)

Distinct variable groups:   x,y,w,h,t,z,f,g,u,v,r,s,a,b,A   B,h,t,f   x,F,y,z,v,u,f,g,h,t,r,s,a,b   h,G,t,f   t,C   y,D,u,v,f,t,a,b   x,R,y,z,w,g,u,v,f,t,s,r,a,b   x,H,u,v,f,t,s,r,a,b

Proof of Theorem zorn2lem7

Step	Hyp	Ref	Expression
1		zorn2lem.1	. . 3 |- A e. V
2	1	weth 4770	. 2 |- E.w w We A
3		zorn2lem.2	. . . . . . . 8 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
4		zorn2lem.3	. . . . . . . 8 |- F = U.B
5		zorn2lem.4	. . . . . . . 8 |- C = {z e. A | A.g e. ran f gRz}
6		zorn2lem.5	. . . . . . . 8 |- D = {z e. A | A.g e. (F"x)gRz}
7		zorn2lem.6	. . . . . . . 8 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
8	1, 3, 4, 5, 6, 7	zorn2lem4 4774	. . . . . . 7 |- ((R Po A /\ w We A) -> E.x e. On D = (/))
9		imaeq2 3398	. . . . . . . . . . . . 13 |- (x = y -> (F"x) = (F"y))
10	9	raleq1d 1787	. . . . . . . . . . . 12 |- (x = y -> (A.g e. (F"x)gRz <-> A.g e. (F"y)gRz))
11	10	rabbisdv 1804	. . . . . . . . . . 11 |- (x = y -> {z e. A | A.g e. (F"x)gRz} = {z e. A | A.g e. (F"y)gRz})
12		zorn2lem.7	. . . . . . . . . . 11 |- H = {z e. A | A.g e. (F"y)gRz}
13	11, 6, 12	3eqtr4g 1529	. . . . . . . . . 10 |- (x = y -> D = H)
14	13	eqeq1d 1481	. . . . . . . . 9 |- (x = y -> (D = (/) <-> H = (/)))
15	14	onminex 3016	. . . . . . . 8 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
16		df-ne 1585	. . . . . . . . . . 11 |- (H =/= (/) <-> -. H = (/))
17	16	ralbii 1665	. . . . . . . . . 10 |- (A.y e. x H =/= (/) <-> A.y e. x -. H = (/))
18	17	anbi2i 480	. . . . . . . . 9 |- ((D = (/) /\ A.y e. x H =/= (/)) <-> (D = (/) /\ A.y e. x -. H = (/)))
19	18	rexbii 1666	. . . . . . . 8 |- (E.x e. On (D = (/) /\ A.y e. x H =/= (/)) <-> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
20	15, 19	sylibr 200	. . . . . . 7 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x H =/= (/)))
21	1, 3, 4, 5, 6, 7, 12	zorn2lem5 4775	. . . . . . . . . . . . . . . . . . . 20 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) (_ A)
22	21	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (F"x) (_ A))
23	1, 3, 4, 5, 6, 7, 12	zorn2lem6 4776	. . . . . . . . . . . . . . . . . . 19 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> R Or (F"x)))
24	22, 23	jcad 599	. . . . . . . . . . . . . . . . . 18 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> ((F"x) (_ A /\ R Or (F"x))))
25	3, 4	tfrlem7 3912	. . . . . . . . . . . . . . . . . . . 20 |- Fun F
26		visset 1810	. . . . . . . . . . . . . . . . . . . . 21 |- x e. V
27	26	funimaex 3572	. . . . . . . . . . . . . . . . . . . 20 |- (Fun F -> (F"x) e. V)
28	25, 27	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- (F"x) e. V
29		sseq1 2079	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (s (_ A <-> (F"x) (_ A))
30		soeq2 2850	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (R Or s <-> R Or (F"x)))
31	29, 30	anbi12d 627	. . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> ((s (_ A /\ R Or s) <-> ((F"x) (_ A /\ R Or (F"x))))
32		raleq1 1784	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (A.r e. s (rRa \/ r = a) <-> A.r e. (F"x)(rRa \/ r = a)))
33	32	rexbidv 1662	. . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> (E.a e. A A.r e. s (rRa \/ r = a) <-> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
34	31, 33	imbi12d 625	. . . . . . . . . . . . . . . . . . 19 |- (s = (F"x) -> (((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a)) <-> (((F"x) (_ A /\ R Or (F"x)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a))))
35	28, 34	cla4v 1865	. . . . . . . . . . . . . . . . . 18 |- (A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a)) -> (((F"x) (_ A /\ R Or (F"x)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
36	24, 35	sylan9 468	. . . . . . . . . . . . . . . . 17 |- ((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
37	36	adantld 390	. . . . . . . . . . . . . . . 16 |- ((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) -> ((D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> E.a e. A A.r e. (F"x)(rRa \/ r = a)))
38	37	imp 350	. . . . . . . . . . . . . . 15 |- (((R Po A /\ A.s((s (_ A /\ R Or s) -> E.a e. A A.r e. s (rRa \/ r = a))) /\ (D = (/) /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/)))) -> E.a e. A A.r e. (F"x)(rRa \/ r = a))
39		noel 2281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- -. b e. (/)
40	21	sseld 2064	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((w We A /\ x e. On) /\ A.y e. x H =/= (/)) -> (r e. (F"x) -> r e. A))
41		potr 2842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((R Po A /\ (r e. A /\ a e. A /\ b e. A)) -> ((rRa /\ aRb) -> rRb))
42		3anass 778	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((r e. A /\ a e. A /\ b e. A) <-> (r e. A /\ (a e. A /\ b e. A)))
43	41, 42	sylan2br 453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> ((rRa /\ aRb) -> rRb))
44	43	exp3a 375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (rRa -> (aRb -> rRb)))
45	44	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (aRb -> (rRa -> rRb)))
46	45	imp 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (rRa -> rRb))
47		breq1 2618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (r = a -> (rRb <-> aRb))
48	47	biimprcd 156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (aRb -> (r = a -> rRb))
49	48	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (r = a -> rRb))
50	46, 49	jaod 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> ((rRa \/ r = a) -> rRb))
51	50	exp42 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (R Po A -> (r e. A -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
52	40, 51	sylan9r 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (r e. (F"x) -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
53	52	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x H =/= (/))) -> (aRb -> (