Theorem zorn2lem4 4771

Description: Lemma for zorn2 4776.

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}}

Assertion

Ref	Expression
zorn2lem4	|- ((R Po A /\ w We A) -> E.x e. On D = (/))

Distinct variable groups:   x,w,h,t,z,f,g,u,v,A   B,h,t,f   x,F,z,v,u,f,g,h,t   h,G,t,f   t,C   u,D,v,f,t   x,R,z,w,g,u,v,f,t

Proof of Theorem zorn2lem4

Step	Hyp	Ref	Expression
1		pm3.24 657	. 2 |- -. (ran F e. V /\ -. ran F e. V)
2		ax-17 969	. . . . . . . . . . 11 |- (w We A -> A.x w We A)
3		hba1 1001	. . . . . . . . . . 11 |- (A.x(x e. On -> D =/= (/)) -> A.xA.x(x e. On -> D =/= (/)))
4	2, 3	hban 1007	. . . . . . . . . 10 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> A.x(w We A /\ A.x(x e. On -> D =/= (/))))
5		ax-17 969	. . . . . . . . . 10 |- (y e. A -> A.x y e. A)
6		eleq1 1531	. . . . . . . . . . . . . . . 16 |- ((F` x) = y -> ((F` x) e. A <-> y e. A))
7		zorn2lem.1	. . . . . . . . . . . . . . . . . 18 |- A e. V
8		zorn2lem.2	. . . . . . . . . . . . . . . . . 18 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
9		zorn2lem.3	. . . . . . . . . . . . . . . . . 18 |- F = U.B
10		zorn2lem.4	. . . . . . . . . . . . . . . . . 18 |- C = {z e. A | A.g e. ran f gRz}
11		zorn2lem.5	. . . . . . . . . . . . . . . . . 18 |- D = {z e. A | A.g e. (F"x)gRz}
12		zorn2lem.6	. . . . . . . . . . . . . . . . . 18 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
13	7, 8, 9, 10, 11, 12	zorn2lem1 4768	. . . . . . . . . . . . . . . . 17 |- ((x e. On /\ (w We A /\ D =/= (/))) -> (F` x) e. D)
14		ssrab2 2127	. . . . . . . . . . . . . . . . . . 19 |- {z e. A | A.g e. (F"x)gRz} (_ A
15	11, 14	eqsstr 2087	. . . . . . . . . . . . . . . . . 18 |- D (_ A
16	15	sseli 2061	. . . . . . . . . . . . . . . . 17 |- ((F` x) e. D -> (F` x) e. A)
17	13, 16	syl 10	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (w We A /\ D =/= (/))) -> (F` x) e. A)
18	6, 17	syl5cbi 209	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (w We A /\ D =/= (/))) -> ((F` x) = y -> y e. A))
19	18	exp32 377	. . . . . . . . . . . . . 14 |- (x e. On -> (w We A -> (D =/= (/) -> ((F` x) = y -> y e. A))))
20	19	com12 11	. . . . . . . . . . . . 13 |- (w We A -> (x e. On -> (D =/= (/) -> ((F` x) = y -> y e. A))))
21	20	a2d 13	. . . . . . . . . . . 12 |- (w We A -> ((x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = y -> y e. A))))
22	21	a4sd 983	. . . . . . . . . . 11 |- (w We A -> (A.x(x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = y -> y e. A))))
23	22	imp 350	. . . . . . . . . 10 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> (x e. On -> ((F` x) = y -> y e. A)))
24	4, 5, 23	r19.23ad 1742	. . . . . . . . 9 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> (E.x e. On (F` x) = y -> y e. A))
25	8, 9	tfr1 3915	. . . . . . . . . 10 |- F Fn On
26		fvelrnb 3751	. . . . . . . . . 10 |- (F Fn On -> (y e. ran F <-> E.x e. On (F` x) = y))
27	25, 26	ax-mp 7	. . . . . . . . 9 |- (y e. ran F <-> E.x e. On (F` x) = y)
28	24, 27	syl5ib 206	. . . . . . . 8 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> (y e. ran F -> y e. A))
29	28	ssrdv 2066	. . . . . . 7 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> ran F (_ A)
30	7	ssex 2714	. . . . . . 7 |- (ran F (_ A -> ran F e. V)
31	29, 30	syl 10	. . . . . 6 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> ran F e. V)
32	31	ex 373	. . . . 5 |- (w We A -> (A.x(x e. On -> D =/= (/)) -> ran F e. V))
33	32	adantl 388	. . . 4 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> ran F e. V))
34	7, 8, 9, 10, 11, 12	zorn2lem3 4770	. . . . . . . . . . . . . 14 |- ((R Po A /\ (x e. On /\ (w We A /\ D =/= (/)))) -> (y e. x -> -. (F` x) = (F` y)))
35	34	exp45 386	. . . . . . . . . . . . 13 |- (R Po A -> (x e. On -> (w We A -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y))))))
36	35	com23 32	. . . . . . . . . . . 12 |- (R Po A -> (w We A -> (x e. On -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y))))))
37	36	imp 350	. . . . . . . . . . 11 |- ((R Po A /\ w We A) -> (x e. On -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y)))))
38	37	a2d 13	. . . . . . . . . 10 |- ((R Po A /\ w We A) -> ((x e. On -> D =/= (/)) -> (x e. On -> (y e. x -> -. (F` x) = (F` y)))))
39	38	imp4a 364	. . . . . . . . 9 |- ((R Po A /\ w We A) -> ((x e. On -> D =/= (/)) -> ((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
40	39	19.21adv 1286	. . . . . . . 8 |- ((R Po A /\ w We A) -> ((x e. On -> D =/= (/)) -> A.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
41	40	19.20dv 1287	. . . . . . 7 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> A.xA.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
42		r2al 1673	. . . . . . 7 |- (A.x e. On A.y e. x -. (F` x) = (F` y) <-> A.xA.y((x e. On /\ y e. x) -> -. (F` x) = (F` y)))
43	41, 42	syl6ibr 213	. . . . . 6 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> A.x e. On A.y e. x -. (F` x) = (F` y)))
44		ssid 2076	. . . . . . . 8 |- On (_ On
45	25	tz7.48lem 3946	. . . . . . . 8 |- ((On (_ On /\ A.x e. On A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` On))
46	44, 45	mpan 694	. . . . . . 7 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'(F |` On))
47	8, 9	tfrlem6 3907	. . . . . . . . . 10 |- Rel F
48		fndm 3579	. . . . . . . . . . . 12 |- (F Fn On -> dom F = On)
49	25, 48	ax-mp 7	. . . . . . . . . . 11 |- dom F = On
50	49	eqimssi 2107	. . . . . . . . . 10 |- dom F (_ On
51		relssres 3384	. . . . . . . . . 10 |- ((Rel F /\ dom F (_ On) -> (F |` On) = F)
52	47, 50, 51	mp2an 696	. . . . . . . . 9 |- (F |` On) = F
53		cnveq 3287	. . . . . . . . 9 |- ((F |` On) = F -> `'(F |` On) = `'F)
54	52, 53	ax-mp 7	. . . . . . . 8 |- `'(F |` On) = `'F
55		funeq 3527	. . . . . . . 8 |- (`'(F |` On) = `'F -> (Fun `'(F |` On) <-> Fun `'F))
56	54, 55	ax-mp 7	. . . . . . 7 |- (Fun `'(F |` On) <-> Fun `'F)
57	46, 56	sylib 198	. . . . . 6 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'F)
58	43, 57	syl6 22	. . . . 5 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> Fun `'F))
59		onprc 2984	. . . . . 6 |- -. On e. V
60		funrnex 3605	. . . . . . . 8 |- (dom `' F e. V -> (Fun `'F -> ran `' F e. V))
61	60	com12 11	. . . . . . 7 |- (Fun `'F -> (dom `' F e. V -> ran `' F e. V))
62		df-rn 3184	. . . . . . . 8 |- ran F = dom `' F
63	62	eleq1i 1534	. . . . . . 7 |- (ran F e. V <-> dom `' F e. V)
64		dfdm4 3300	. . . . . . . . 9 |- dom F = ran `' F
65	49, 64	eqtr3 1494	. . . . . . . 8 |- On = ran `' F
66	65	eleq1i 1534	. . . . . . 7 |- (On e. V <-> ran `' F e. V)
67	61, 63, 66	3imtr4g 552	. . . . . 6 |- (Fun `'F -> (ran F e. V -> On e. V))
68	59, 67	mtoi 107	. . . . 5 |- (Fun `'F -> -. ran F e. V)
69	58, 68	syl6 22	. . . 4 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> -. ran F e. V))
70	33, 69	jcad 599	. . 3 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> (ran F e. V /\ -. ran F e. V)))
71		df-ne 1584	. . . . 5 |- (D =/= (/) <-> -. D = (/))
72	71	ralbii 1664	. . . 4 |- (A.x e. On D =/= (/) <-> A.x e. On -. D = (/))
73		df-ral 1646	. . . 4 |- (A.x e. On D =/= (/) <-> A.x(x e. On -> D =/= (/)))
74		ralnex 1650	.