Theorem zorn2lem4 6364

Description: Lemma for zorn2 6369.

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 972	. 2 |- -. (ran F e. _V /\ -. ran F e. _V)
2		df-ne 2268	. . . . 5 |- (D =/= (/) <-> -. D = (/))
3	2	ralbii 2377	. . . 4 |- (A.x e. On D =/= (/) <-> A.x e. On -. D = (/))
4		df-ral 2359	. . . 4 |- (A.x e. On D =/= (/) <-> A.x(x e. On -> D =/= (/)))
5		ralnex 2363	. . . 4 |- (A.x e. On -. D = (/) <-> -. E.x e. On D = (/))
6	3, 4, 5	3bitr3i 293	. . 3 |- (A.x(x e. On -> D =/= (/)) <-> -. E.x e. On D = (/))
7		zorn2lem.2	. . . . . . . . . . 11 |- B = {f | E.h e. On (f Fn h /\ A.t e. h (f` t) = (G` (f |` t)))}
8		zorn2lem.3	. . . . . . . . . . 11 |- F = U.B
9	7, 8	tfr1 5296	. . . . . . . . . 10 |- F Fn On
10		fvelrnb 4805	. . . . . . . . . 10 |- (F Fn On -> (y e. ran F <-> E.x e. On (F` x) = y))
11	9, 10	ax-mp 7	. . . . . . . . 9 |- (y e. ran F <-> E.x e. On (F` x) = y)
12		ax-17 1605	. . . . . . . . . . 11 |- (w We A -> A.x w We A)
13		hba1 1639	. . . . . . . . . . 11 |- (A.x(x e. On -> D =/= (/)) -> A.xA.x(x e. On -> D =/= (/)))
14	12, 13	hban 1645	. . . . . . . . . 10 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> A.x(w We A /\ A.x(x e. On -> D =/= (/))))
15		ax-17 1605	. . . . . . . . . 10 |- (y e. A -> A.x y e. A)
16		zorn2lem.1	. . . . . . . . . . . . . . . . . 18 |- A e. _V
17		zorn2lem.4	. . . . . . . . . . . . . . . . . 18 |- C = {z e. A | A.g e. ran f gRz}
18		zorn2lem.5	. . . . . . . . . . . . . . . . . 18 |- D = {z e. A | A.g e. (F"x)gRz}
19		zorn2lem.6	. . . . . . . . . . . . . . . . . 18 |- G = {<.f, t>. | t = U.{v e. C | A.u e. C -. uwv}}
20	16, 7, 8, 17, 18, 19	zorn2lem1 6361	. . . . . . . . . . . . . . . . 17 |- ((x e. On /\ (w We A /\ D =/= (/))) -> (F` x) e. D)
21		ssrab2 2917	. . . . . . . . . . . . . . . . . . 19 |- {z e. A | A.g e. (F"x)gRz} C_ A
22	18, 21	eqsstri 2874	. . . . . . . . . . . . . . . . . 18 |- D C_ A
23	22	sseli 2848	. . . . . . . . . . . . . . . . 17 |- ((F` x) e. D -> (F` x) e. A)
24	20, 23	syl 13	. . . . . . . . . . . . . . . 16 |- ((x e. On /\ (w We A /\ D =/= (/))) -> (F` x) e. A)
25		eleq1 2204	. . . . . . . . . . . . . . . 16 |- ((F` x) = y -> ((F` x) e. A <-> y e. A))
26	24, 25	syl5ibcom 254	. . . . . . . . . . . . . . 15 |- ((x e. On /\ (w We A /\ D =/= (/))) -> ((F` x) = y -> y e. A))
27	26	exp32 578	. . . . . . . . . . . . . 14 |- (x e. On -> (w We A -> (D =/= (/) -> ((F` x) = y -> y e. A))))
28	27	com12 26	. . . . . . . . . . . . 13 |- (w We A -> (x e. On -> (D =/= (/) -> ((F` x) = y -> y e. A))))
29	28	a2d 19	. . . . . . . . . . . 12 |- (w We A -> ((x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = y -> y e. A))))
30	29	a4sd 1620	. . . . . . . . . . 11 |- (w We A -> (A.x(x e. On -> D =/= (/)) -> (x e. On -> ((F` x) = y -> y e. A))))
31	30	imp 393	. . . . . . . . . 10 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> (x e. On -> ((F` x) = y -> y e. A)))
32	14, 15, 31	r19.23ad 2462	. . . . . . . . 9 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> (E.x e. On (F` x) = y -> y e. A))
33	11, 32	syl5bi 249	. . . . . . . 8 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> (y e. ran F -> y e. A))
34	33	ssrdv 2853	. . . . . . 7 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> ran F C_ A)
35	16	ssex 3622	. . . . . . 7 |- (ran F C_ A -> ran F e. _V)
36	34, 35	syl 13	. . . . . 6 |- ((w We A /\ A.x(x e. On -> D =/= (/))) -> ran F e. _V)
37	36	ex 398	. . . . 5 |- (w We A -> (A.x(x e. On -> D =/= (/)) -> ran F e. _V))
38	37	adantl 448	. . . 4 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> ran F e. _V))
39	16, 7, 8, 17, 18, 19	zorn2lem3 6363	. . . . . . . . . . . . . 14 |- ((R Po A /\ (x e. On /\ (w We A /\ D =/= (/)))) -> (y e. x -> -. (F` x) = (F` y)))
40	39	exp45 588	. . . . . . . . . . . . 13 |- (R Po A -> (x e. On -> (w We A -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y))))))
41	40	com23 65	. . . . . . . . . . . 12 |- (R Po A -> (w We A -> (x e. On -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y))))))
42	41	imp 393	. . . . . . . . . . 11 |- ((R Po A /\ w We A) -> (x e. On -> (D =/= (/) -> (y e. x -> -. (F` x) = (F` y)))))
43	42	a2d 19	. . . . . . . . . 10 |- ((R Po A /\ w We A) -> ((x e. On -> D =/= (/)) -> (x e. On -> (y e. x -> -. (F` x) = (F` y)))))
44	43	imp4a 565	. . . . . . . . 9 |- ((R Po A /\ w We A) -> ((x e. On -> D =/= (/)) -> ((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
45	44	19.21adv 1935	. . . . . . . 8 |- ((R Po A /\ w We A) -> ((x e. On -> D =/= (/)) -> A.y((x e. On /\ y e. x) -> -. (F` x) = (F` y))))
46	45	alimdv 1937	. . . . . . 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))))
47		r2al 2386	. . . . . . 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)))
48	46, 47	syl6ibr 262	. . . . . 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)))
49		ssid 2863	. . . . . . . 8 |- On C_ On
50	9	tz7.48lem 5328	. . . . . . . 8 |- ((On C_ On /\ A.x e. On A.y e. x -. (F` x) = (F` y)) -> Fun `'(F |` On))
51	49, 50	mpan 677	. . . . . . 7 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'(F |` On))
52	7, 8	tfrlem6 5288	. . . . . . . . . 10 |- Rel F
53		fndm 4612	. . . . . . . . . . . 12 |- (F Fn On -> dom F = On)
54	9, 53	ax-mp 7	. . . . . . . . . . 11 |- dom F = On
55	54	eqimssi 2896	. . . . . . . . . 10 |- dom F C_ On
56		relssres 4370	. . . . . . . . . 10 |- ((Rel F /\ dom F C_ On) -> (F |` On) = F)
57	52, 55, 56	mp2an 681	. . . . . . . . 9 |- (F |` On) = F
58	57	cnveqi 4264	. . . . . . . 8 |- `'(F |` On) = `'F
59		funeq 4544	. . . . . . . 8 |- (`'(F |` On) = `'F -> (Fun `'(F |` On) <-> Fun `'F))
60	58, 59	ax-mp 7	. . . . . . 7 |- (Fun `'(F |` On) <-> Fun `'F)
61	51, 60	sylib 242	. . . . . 6 |- (A.x e. On A.y e. x -. (F` x) = (F` y) -> Fun `'F)
62	48, 61	syl6 42	. . . . 5 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> Fun `'F))
63		onprc 4010	. . . . . 6 |- -. On e. _V
64		funrnex 4640	. . . . . . . 8 |- (dom `' F e. _V -> (Fun `'F -> ran `' F e. _V))
65	64	com12 26	. . . . . . 7 |- (Fun `'F -> (dom `' F e. _V -> ran `' F e. _V))
66		df-rn 4138	. . . . . . . 8 |- ran F = dom `' F
67	66	eleq1i 2207	. . . . . . 7 |- (ran F e. _V <-> dom `' F e. _V)
68		dfdm4 4277	. . . . . . . . 9 |- dom F = ran `' F
69	54, 68	eqtr3i 2163	. . . . . . . 8 |- On = ran `' F
70	69	eleq1i 2207	. . . . . . 7 |- (On e. _V <-> ran `' F e. _V)
71	65, 67, 70	3imtr4g 332	. . . . . 6 |- (Fun `'F -> (ran F e. _V -> On e. _V))
72	63, 71	mtoi 153	. . . . 5 |- (Fun `'F -> -. ran F e. _V)
73	62, 72	syl6 42	. . . 4 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> -. ran F e. _V))
74	38, 73	jcad 496	. . 3 |- ((R Po A /\ w We A) -> (A.x(x e. On -> D =/= (/)) -> (ran F e. _V /\ -. ran F e. _V)))
75	6, 74	syl5bir 251	. 2 |- ((R Po A /\ w We A) -> (-. E.x e. On D = (/) -> (ran F e. _V /\ -. ran F e. _V)))
76	1, 75	mt3i 161	1 |- ((R Po A /\ w We A) -> E.x e. On D = (/))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  {cab 2128   =/= wne 2266  A.wral 2355  E.wrex 2356  {crab 2358  _Vcvv 2538   C_ wss 2827  (/)c0 3082  U.cuni 3366   class class class wbr 3507  {copab 3565   Po wpo 3750   We wwe 3781  Oncon0 3811  `'ccnv 4118  dom cdm 4119  ran crn 4120   |` cres 4121  "cima 4122  Rel wrel 4124  Fun wfun 4125   Fn wfn 4126  ` cfv 4131

This theorem is referenced by:  zorn2lem7 6367

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-suc 3817  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fv 4147

Copyright terms: Public domain