Theorem zornlem4 3606

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

Assertion

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

Distinct variable group(s):   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 zornlem4

Step	Hyp	Ref	Expression
1		pm3.24 496	. . 3 |- -. (ran F e. V /\ -. ran F e. V)
2		ax-17 925	. . . . . . . . . . . 12 |- (w We A -> A.x w We A)
3		hba1 698	. . . . . . . . . . . 12 |- (A.x(x e. On -> -. D = (/)) -> A.xA.x(x e. On -> -. D = (/)))
4	2, 3	hban 704	. . . . . . . . . . 11 |- ((w We A /\ A.x(x e. On -> -. D = (/))) -> A.x(w We A /\ A.x(x e. On -> -. D = (/))))
5		ax-17 925	. . . . . . . . . . 11 |- (y e. A -> A.x y e. A)
6		eleq1 1149	. . . . . . . . . . . . . . . . . 18 |- ((F` x) = y -> ((F` x) e. A <-> y e. A))
7		zornlem.1	. . . . . . . . . . . . . . . . . . . 20 |- A e. V
8		zornlem.2	. . . . . . . . . . . . . . . . . . . 20 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
9		zornlem.3	. . . . . . . . . . . . . . . . . . . 20 |- F = U.B
10		zornlem.4	. . . . . . . . . . . . . . . . . . . 20 |- C = {z e. A | A.g e. ran fgRz}
11		zornlem.5	. . . . . . . . . . . . . . . . . . . 20 |- D = {z e. A | A.g e. (F"x)gRz}
12		zornlem.6	. . . . . . . . . . . . . . . . . . . 20 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
13	7, 8, 9, 10, 11, 12	zornlem1 3603	. . . . . . . . . . . . . . . . . . 19 |- ((x e. On /\ (w We A /\ -. D = (/))) -> (F` x) e. D)
14		ssrab 1556	. . . . . . . . . . . . . . . . . . . . 21 |- {z e. A | A.g e. (F"x)gRz} (_ A
15	11, 14	eqsstr 1530	. . . . . . . . . . . . . . . . . . . 20 |- D (_ A
16	15	sseli 1504	. . . . . . . . . . . . . . . . . . 19 |- ((F` x) e. D -> (F` x) e. A)
17	13, 16	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((x e. On /\ (w We A /\ -. D = (/))) -> (F` x) e. A)
18	6, 17	syl5bi 183	. . . . . . . . . . . . . . . . 17 |- ((F` x) = y -> ((x e. On /\ (w We A /\ -. D = (/))) -> y e. A))
19	18	com12 13	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (w We A /\ -. D = (/))) -> ((F` x) = y -> y e. A))
20	19	exp32 294	. . . . . . . . . . . . . . 15 |- (x e. On -> (w We A -> (-. D = (/) -> ((F` x) = y -> y e. A))))
21	20	com12 13	. . . . . . . . . . . . . 14 |- (w We A -> (x e. On -> (-. D = (/) -> ((F` x) = y -> y e. A))))
22	21	a2d 15	. . . . . . . . . . . . 13 |- (w We A -> ((x e. On -> -. D = (/)) -> (x e. On -> ((F` x) = y -> y e. A))))
23	22	a4sd 683	. . . . . . . . . . . 12 |- (w We A -> (A.x(x e. On -> -. D = (/)) -> (x e. On -> ((F` x) = y -> y e. A))))
24	23	imp 277	. . . . . . . . . . 11 |- ((w We A /\ A.x(x e. On -> -. D = (/))) -> (x e. On -> ((F` x) = y -> y e. A)))
25	4, 5, 24	r19.23ad 1285	. . . . . . . . . 10 |- ((w We A /\ A.x(x e. On -> -. D = (/))) -> (E.x e. On (F` x) = y -> y e. A))
26	8, 9	tfr1 2962	. . . . . . . . . . 11 |- F Fn On
27		fvelrn 2883	. . . . . . . . . . 11 |- (F Fn On -> (y e. ran F <-> E.x e. On (F` x) = y))
28	26, 27	ax-mp 6	. . . . . . . . . 10 |- (y e. ran F <-> E.x e. On (F` x) = y)
29	25, 28	syl5ib 181	. . . . . . . . 9 |- ((w We A /\ A.x(x e. On -> -. D = (/))) -> (y e. ran F -> y e. A))
30	29	ssrdv 1509	. . . . . . . 8 |- ((w We A /\ A.x(x e. On -> -. D = (/))) -> ran F (_ A)
31	7	ssex 1700	. . . . . . . 8 |- (ran F (_ A -> ran F e. V)
32	30, 31	syl 12	. . . . . . 7 |- ((w We A /\ A.x(x e. On -> -. D = (/))) -> ran F e. V)
33	32	exp 291	. . . . . 6 |- (w We A -> (A.x(x e. On -> -. D = (/)) -> ran F e. V))
34	33	adantl 305	. . . . 5 |- ((R Po A /\ w We A) -> (A.x(x e. On -> -. D = (/)) -> ran F e. V))
35	7, 8, 9, 10, 11, 12	zornlem3 3605	. . . . . . . . . . . . . . 15 |- ((R Po A /\ (x e. On /\ (w We A /\ -. D = (/)))) -> (y e. x -> -. (F` x) = (F` y)))
36	35	exp45 303	. . . . . . . . . . . . . 14 |- (R Po A -> (x e. On -> (w We A -> (-. D = (/) -> (y e. x -> -. (F` x) = (F` y))))))
37	36	com23 32	. . . . . . . . . . . . 13 |- (R Po A -> (w We A -> (x e. On -> (-. D = (/) -> (y e. x -> -. (F` x) = (F` y))))))
38	37	imp 277	. . . . . . . . . . . 12 |- ((R Po A /\ w We A) -> (x e. On -> (-. D = (/) -> (y e. x -> -. (F` x) = (F` y)))))
39	38	a2d 15	. . . . . . . . . . 11 |- ((R Po A /\ w We A) -> ((x e. On -> -. D = (/)) -> (x e. On -> (y e. x -> -. (F` x) = (F` y)))))
40	39	imp4a 282	. . . . . . . . . 10 |- ((R Po A /\ w We A) -> ((x e. On -> -. D = (/)) -> ((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
41	40	19.21adv 945	. . . . . . . . 9 |- ((R Po A /\ w We A) -> ((x e. On -> -. D = (/)) -> A.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
42	41	19.20dv 946	. . . . . . . 8 |- ((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))))
43		r2al 1231	. . . . . . . 8 |- (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)))
44	42, 43	syl6ibr 186	. . . . . . 7 |- ((R Po A /\ w We A) -> (A.x(x e. On -> -. D = (/)) -> A.x e. On A.y e. x -. (F` x) = (F` y)))
45		ssid 1519	. . . . . . . . 9 |- On (_ On
46	26	tz7.48lem 2993	. . . . . . . . 9 |- ((On (_ On /\ A.x e. On A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` On))
47	45, 46	mpan 518	. . . . . . . 8 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'(F |` On))
48	8, 9	tfrlem6 2954	. . . . . . . . . . 11 |- Rel F
49		fndm 2723	. . . . . . . . . . . . 13 |- (F Fn On -> dom F = On)
50	26, 49	ax-mp 6	. . . . . . . . . . . 12 |- dom F = On
51	50, 45	eqsstr 1530	. . . . . . . . . . 11 |- dom F (_ On
52		relssres 2596	. . . . . . . . . . 11 |- ((Rel F /\ dom F (_ On) -> (F |` On) = F)
53	48, 51, 52	mp2an 520	. . . . . . . . . 10 |- (F |` On) = F
54		cnveq 2513	. . . . . . . . . 10 |- ((F |` On) = F -> `'(F |` On) = `'F)
55	53, 54	ax-mp 6	. . . . . . . . 9 |- `'(F |` On) = `'F
56		funeq 2683	. . . . . . . . 9 |- (`'(F |` On) = `'F -> (Fun `'(F |` On) <-> Fun `'F))
57	55, 56	ax-mp 6	. . . . . . . 8 |- (Fun `'(F |` On) <-> Fun `'F)
58	47, 57	sylib 173	. . . . . . 7 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'F)
59	44, 58	syl6 23	. . . . . 6 |- ((R Po A /\ w We A) -> (A.x(x e. On -> -. D = (/)) -> Fun `'F))
60		onprc 2240	. . . . . . 7 |- -. On e. V
61		funrnex 2743	. . . . . . . . 9 |- (dom `'F e. V -> (Fun `'F -> ran `'F e. V))
62	61	com12 13	. . . . . . . 8 |- (Fun `'F -> (dom `'F e. V -> ran `'F e. V))
63		df-rn 2429	. . . . . . . . 9 |- ran F = dom `'F
64	63	eleq1i 1152	. . . . . . . 8 |- (ran F e. V <-> dom `'F e. V)
65		dfdm4 2525	. . . . . . . . . 10 |- dom F = ran `'F
66	50, 65	eqtr3 1121	. . . . . . . . 9 |- On = ran `'F
67	66	eleq1i 1152	. . . . . . . 8 |- (On e. V <-> ran `'F e. V)
68	62, 64, 67	3imtr4g 426	. . . . . . 7 |- (Fun `'F -> (ran F e. V -> On e. V))
69	60, 68	mtoi 94	. . . . . 6 |- (Fun `'F -> -. ran F e. V)
70	59, 69	syl6 23	. . . . 5 |- ((R Po A /\ w We A) -> (A.x(x e. On -> -. D = (/)) -> -. ran F e. V))
71	34, 70	jcad 455	. . . 4 |- ((R Po A /\ w We A) -> (A.x(x e. On -> -. D = (/)) -> (ran F e. V /\ -. ran F e. V)))
72		alinexa 724	. . . 4 |- (A.x(x e. On -> -. D = (/)) <-> -. E.x(x e. On /\ D = (/)))
73	71, 72	syl5ibr 182	. . 3 |- ((R Po A /\ w We A) -> (-. E.x(x e. On /\ D = (/)) -> (ran F e. V /\ -. ran F e. V)))
74	1, 73	mt3i 100	. 2 |- (