Theorem zornlem7 3609

Description: Lemma for Zorn's lemma.

Hypotheses

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

Assertion

Ref	Expression
zornlem7	|- ((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 group(s):   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 zornlem7

Step	Hyp	Ref	Expression
1		zornlem.1	. . 3 |- A e. V
2	1	weth 3602	. 2 |- E.w w We A
3		zornlem.2	. . . . . . . 8 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
4		zornlem.3	. . . . . . . 8 |- F = U.B
5		zornlem.4	. . . . . . . 8 |- C = {z e. A | A.g e. ran fgRz}
6		zornlem.5	. . . . . . . 8 |- D = {z e. A | A.g e. (F"x)gRz}
7		zornlem.6	. . . . . . . 8 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
8	1, 3, 4, 5, 6, 7	zornlem4 3606	. . . . . . 7 |- ((R Po A /\ w We A) -> E.x e. On D = (/))
9		imaeq2 2603	. . . . . . . . . . . 12 |- (x = y -> (F"x) = (F"y))
10		raleq 1324	. . . . . . . . . . . 12 |- ((F"x) = (F"y) -> (A.g e. (F"x)gRz <-> A.g e. (F"y)gRz))
11	9, 10	syl 12	. . . . . . . . . . 11 |- (x = y -> (A.g e. (F"x)gRz <-> A.g e. (F"y)gRz))
12	11	birabsdv 1344	. . . . . . . . . 10 |- (x = y -> {z e. A | A.g e. (F"x)gRz} = {z e. A | A.g e. (F"y)gRz})
13		zornlem.7	. . . . . . . . . 10 |- H = {z e. A | A.g e. (F"y)gRz}
14	12, 6, 13	3eqtr4g 1147	. . . . . . . . 9 |- (x = y -> D = H)
15	14	cleq1d 1109	. . . . . . . 8 |- (x = y -> (D = (/) <-> H = (/)))
16	15	onminex 2275	. . . . . . 7 |- (E.x e. On D = (/) -> E.x e. On (D = (/) /\ A.y e. x -. H = (/)))
17	1, 3, 4, 5, 6, 7, 13	zornlem5 3607	. . . . . . . . . . . . . . . . . . . 20 |- (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> (F"x) (_ A)
18	17	a1i 7	. . . . . . . . . . . . . . . . . . 19 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> (F"x) (_ A))
19	1, 3, 4, 5, 6, 7, 13	zornlem6 3608	. . . . . . . . . . . . . . . . . . 19 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> R Or (F"x)))
20	18, 19	jcad 455	. . . . . . . . . . . . . . . . . 18 |- (R Po A -> (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> ((F"x) (_ A /\ R Or (F"x))))
21	3, 4	tfrlem7 2955	. . . . . . . . . . . . . . . . . . . 20 |- Fun F
22		visset 1350	. . . . . . . . . . . . . . . . . . . . 21 |- x e. V
23	22	funimaex 2716	. . . . . . . . . . . . . . . . . . . 20 |- (Fun F -> (F"x) e. V)
24	21, 23	ax-mp 6	. . . . . . . . . . . . . . . . . . 19 |- (F"x) e. V
25		sseq1 1521	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (s (_ A <-> (F"x) (_ A))
26		soeq2 2142	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (R Or s <-> R Or (F"x)))
27	25, 26	anbi12d 476	. . . . . . . . . . . . . . . . . . . 20 |- (s = (F"x) -> ((s (_ A /\ R Or s) <-> ((F"x) (_ A /\ R Or (F"x))))
28		raleq 1324	. . . . . . . . . . . . . . . . . . . . 21 |- (s = (F"x) -> (A.r e. s (rRa \/ r = a) <-> A.r e. (F"x)(rRa \/ r = a)))
29	28	birexdv 1220	. . . . . . . . . . . . . . . . . . . 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)))
30	27, 29	imbi12d 474	. . . . . . . . . . . . . . . . . . 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))))
31	24, 30	cla4v 1400	. . . . . . . . . . . . . . . . . 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)))
32	20, 31	sylan9 359	. . . . . . . . . . . . . . . . 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)))
33	32	adantld 307	. . . . . . . . . . . . . . . 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)))
34	33	imp 277	. . . . . . . . . . . . . . 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))
35		noel 1711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- -. b e. (/)
36	17	sseld 1506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (((w We A /\ x e. On) /\ A.y e. x -. H = (/)) -> (r e. (F"x) -> r e. A))
37		potr 2134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((R Po A /\ (r e. A /\ a e. A /\ b e. A)) -> ((rRa /\ aRb) -> rRb))
38		3anass 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 |- ((r e. A /\ a e. A /\ b e. A) <-> (r e. A /\ (a e. A /\ b e. A)))
39	37, 38	sylan2br 348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> ((rRa /\ aRb) -> rRb))
40	39	exp3a 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (rRa -> (aRb -> rRb)))
41	40	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- ((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) -> (aRb -> (rRa -> rRb)))
42	41	imp 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (rRa -> rRb))
43		breq1 2065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 |- (r = a -> (rRb <-> aRb))
44	43	biimprcd 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 |- (aRb -> (r = a -> rRb))
45	44	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> (r = a -> rRb))
46	42, 45	jaod 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 |- (((R Po A /\ (r e. A /\ (a e. A /\ b e. A))) /\ aRb) -> ((rRa \/ r = a) -> rRb))
47	46	exp42 300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 |- (R Po A -> (r e. A -> ((a e. A /\ b e. A) -> (aRb -> ((rRa \/ r = a) -> rRb)))))
48	36, 47	sylan9r 360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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)))))
49	48	com24 37	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x -. H = (/))) -> (aRb -> ((a e. A /\ b e. A) -> (r e. (F"x) -> ((rRa \/ r = a) -> rRb)))))
50	49	com23 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 |- ((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x -. H = (/))) -> ((a e. A /\ b e. A) -> (aRb -> (r e. (F"x) -> ((rRa \/ r = a) -> rRb)))))
51	50	imp31 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 |- ((((R Po A /\ ((w We A /\ x e. On) /\ A.y e. x -. H = (/))) /\ (