Theorem zorn2lem4 4801

Description: Lemma for zorn2 4806.

Hypotheses

Ref	Expression
zorn2lem.1	⊢ A ∈ V
zorn2lem.2	⊢ B = {f∣∃h ∈ On (f Fn h ⋀ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
zorn2lem.3	⊢ F = ∪B
zorn2lem.4	⊢ C = {z ∈ A∣∀g ∈ ran f gRz}
zorn2lem.5	⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
zorn2lem.6	⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}

Assertion

Ref	Expression
zorn2lem4	⊢ ((R Po A ⋀ w We A) → ∃x ∈ 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 660	. 2 ⊢ ¬ (ran F ∈ V ⋀ ¬ ran F ∈ V)
2		ax-17 973	. . . . . . . . . . 11 ⊢ (w We A → ∀x w We A)
3		hba1 1005	. . . . . . . . . . 11 ⊢ (∀x(x ∈ On → D ≠ ∅) → ∀x∀x(x ∈ On → D ≠ ∅))
4	2, 3	hban 1011	. . . . . . . . . 10 ⊢ ((w We A ⋀ ∀x(x ∈ On → D ≠ ∅)) → ∀x(w We A ⋀ ∀x(x ∈ On → D ≠ ∅)))
5		ax-17 973	. . . . . . . . . 10 ⊢ (y ∈ A → ∀x y ∈ A)
6		eleq1 1537	. . . . . . . . . . . . . . . 16 ⊢ ((F ‘x) = y → ((F ‘x) ∈ A ↔ y ∈ A))
7		zorn2lem.1	. . . . . . . . . . . . . . . . . 18 ⊢ A ∈ V
8		zorn2lem.2	. . . . . . . . . . . . . . . . . 18 ⊢ B = {f∣∃h ∈ On (f Fn h ⋀ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
9		zorn2lem.3	. . . . . . . . . . . . . . . . . 18 ⊢ F = ∪B
10		zorn2lem.4	. . . . . . . . . . . . . . . . . 18 ⊢ C = {z ∈ A∣∀g ∈ ran f gRz}
11		zorn2lem.5	. . . . . . . . . . . . . . . . . 18 ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
12		zorn2lem.6	. . . . . . . . . . . . . . . . . 18 ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
13	7, 8, 9, 10, 11, 12	zorn2lem1 4798	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ On ⋀ (w We A ⋀ D ≠ ∅)) → (F ‘x) ∈ D)
14		ssrab2 2134	. . . . . . . . . . . . . . . . . . 19 ⊢ {z ∈ A∣∀g ∈ (F “ x)gRz} ⊆ A
15	11, 14	eqsstr 2094	. . . . . . . . . . . . . . . . . 18 ⊢ D ⊆ A
16	15	sseli 2068	. . . . . . . . . . . . . . . . 17 ⊢ ((F ‘x) ∈ D → (F ‘x) ∈ A)
17	13, 16	syl 10	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ⋀ (w We A ⋀ D ≠ ∅)) → (F ‘x) ∈ A)
18	6, 17	syl5cbi 209	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ On ⋀ (w We A ⋀ D ≠ ∅)) → ((F ‘x) = y → y ∈ A))
19	18	exp32 379	. . . . . . . . . . . . . 14 ⊢ (x ∈ On → (w We A → (D ≠ ∅ → ((F ‘x) = y → y ∈ A))))
20	19	com12 11	. . . . . . . . . . . . 13 ⊢ (w We A → (x ∈ On → (D ≠ ∅ → ((F ‘x) = y → y ∈ A))))
21	20	a2d 13	. . . . . . . . . . . 12 ⊢ (w We A → ((x ∈ On → D ≠ ∅) → (x ∈ On → ((F ‘x) = y → y ∈ A))))
22	21	a4sd 987	. . . . . . . . . . 11 ⊢ (w We A → (∀x(x ∈ On → D ≠ ∅) → (x ∈ On → ((F ‘x) = y → y ∈ A))))
23	22	imp 350	. . . . . . . . . 10 ⊢ ((w We A ⋀ ∀x(x ∈ On → D ≠ ∅)) → (x ∈ On → ((F ‘x) = y → y ∈ A)))
24	4, 5, 23	r19.23ad 1748	. . . . . . . . 9 ⊢ ((w We A ⋀ ∀x(x ∈ On → D ≠ ∅)) → (∃x ∈ On (F ‘x) = y → y ∈ A))
25	8, 9	tfr1 3930	. . . . . . . . . 10 ⊢ F Fn On
26		fvelrnb 3766	. . . . . . . . . 10 ⊢ (F Fn On → (y ∈ ran F ↔ ∃x ∈ On (F ‘x) = y))
27	25, 26	ax-mp 7	. . . . . . . . 9 ⊢ (y ∈ ran F ↔ ∃x ∈ On (F ‘x) = y)
28	24, 27	syl5ib 206	. . . . . . . 8 ⊢ ((w We A ⋀ ∀x(x ∈ On → D ≠ ∅)) → (y ∈ ran F → y ∈ A))
29	28	ssrdv 2073	. . . . . . 7 ⊢ ((w We A ⋀ ∀x(x ∈ On → D ≠ ∅)) → ran F ⊆ A)
30	7	ssex 2724	. . . . . . 7 ⊢ (ran F ⊆ A → ran F ∈ V)
31	29, 30	syl 10	. . . . . 6 ⊢ ((w We A ⋀ ∀x(x ∈ On → D ≠ ∅)) → ran F ∈ V)
32	31	ex 373	. . . . 5 ⊢ (w We A → (∀x(x ∈ On → D ≠ ∅) → ran F ∈ V))
33	32	adantl 390	. . . 4 ⊢ ((R Po A ⋀ w We A) → (∀x(x ∈ On → D ≠ ∅) → ran F ∈ V))
34	7, 8, 9, 10, 11, 12	zorn2lem3 4800	. . . . . . . . . . . . . 14 ⊢ ((R Po A ⋀ (x ∈ On ⋀ (w We A ⋀ D ≠ ∅))) → (y ∈ x → ¬ (F ‘x) = (F ‘y)))
35	34	exp45 388	. . . . . . . . . . . . 13 ⊢ (R Po A → (x ∈ On → (w We A → (D ≠ ∅ → (y ∈ x → ¬ (F ‘x) = (F ‘y))))))
36	35	com23 32	. . . . . . . . . . . 12 ⊢ (R Po A → (w We A → (x ∈ On → (D ≠ ∅ → (y ∈ x → ¬ (F ‘x) = (F ‘y))))))
37	36	imp 350	. . . . . . . . . . 11 ⊢ ((R Po A ⋀ w We A) → (x ∈ On → (D ≠ ∅ → (y ∈ x → ¬ (F ‘x) = (F ‘y)))))
38	37	a2d 13	. . . . . . . . . 10 ⊢ ((R Po A ⋀ w We A) → ((x ∈ On → D ≠ ∅) → (x ∈ On → (y ∈ x → ¬ (F ‘x) = (F ‘y)))))
39	38	imp4a 364	. . . . . . . . 9 ⊢ ((R Po A ⋀ w We A) → ((x ∈ On → D ≠ ∅) → ((x ∈ On ⋀ y ∈ x) → ¬ (F ‘x) = (F ‘y))))
40	39	19.21adv 1290	. . . . . . . 8 ⊢ ((R Po A ⋀ w We A) → ((x ∈ On → D ≠ ∅) → ∀y((x ∈ On ⋀ y ∈ x) → ¬ (F ‘x) = (F ‘y))))
41	40	19.20dv 1291	. . . . . . 7 ⊢ ((R Po A ⋀ w We A) → (∀x(x ∈ On → D ≠ ∅) → ∀x∀y((x ∈ On ⋀ y ∈ x) → ¬ (F ‘x) = (F ‘y))))
42		r2al 1679	. . . . . . 7 ⊢ (∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y) ↔ ∀x∀y((x ∈ On ⋀ y ∈ x) → ¬ (F ‘x) = (F ‘y)))
43	41, 42	syl6ibr 213	. . . . . 6 ⊢ ((R Po A ⋀ w We A) → (∀x(x ∈ On → D ≠ ∅) → ∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y)))
44		ssid 2083	. . . . . . . 8 ⊢ On ⊆ On
45	25	tz7.48lem 3961	. . . . . . . 8 ⊢ ((On ⊆ On ⋀ ∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y)) → Fun ◡(F ↾ On))
46	44, 45	mpan 697	. . . . . . 7 ⊢ (∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y) → Fun ◡(F ↾ On))
47	8, 9	tfrlem6 3922	. . . . . . . . . 10 ⊢ Rel F
48		fndm 3593	. . . . . . . . . . . 12 ⊢ (F Fn On → dom F = On)
49	25, 48	ax-mp 7	. . . . . . . . . . 11 ⊢ dom F = On
50	49	eqimssi 2114	. . . . . . . . . 10 ⊢ dom F ⊆ On
51		relssres 3398	. . . . . . . . . 10 ⊢ ((Rel F ⋀ dom F ⊆ On) → (F ↾ On) = F)
52	47, 50, 51	mp2an 699	. . . . . . . . 9 ⊢ (F ↾ On) = F
53		cnveq 3298	. . . . . . . . 9 ⊢ ((F ↾ On) = F → ◡(F ↾ On) = ◡F)
54	52, 53	ax-mp 7	. . . . . . . 8 ⊢ ◡(F ↾ On) = ◡F
55		funeq 3541	. . . . . . . 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 ⊢ (∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y) → Fun ◡F)
58	43, 57	syl6 22	. . . . 5 ⊢ ((R Po A ⋀ w We A) → (∀x(x ∈ On → D ≠ ∅) → Fun ◡F))
59		onprc 2995	. . . . . 6 ⊢ ¬ On ∈ V
60		funrnex 3619	. . . . . . . 8 ⊢ (dom ◡ F ∈ V → (Fun ◡F → ran ◡ F ∈ V))
61	60	com12 11	. . . . . . 7 ⊢ (Fun ◡F → (dom ◡ F ∈ V → ran ◡ F ∈ V))
62		df-rn 3195	. . . . . . . 8 ⊢ ran F = dom ◡ F
63	62	eleq1i 1540	. . . . . . 7 ⊢ (ran F ∈ V ↔ dom ◡ F ∈ V)
64		dfdm4 3311	. . . . . . . . 9 ⊢ dom F = ran ◡ F
65	49, 64	eqtr3 1500	. . . . . . . 8 ⊢ On = ran ◡ F
66	65	eleq1i 1540	. . . . . . 7 ⊢ (On ∈ V ↔ ran ◡ F ∈ V)
67	61, 63, 66	3imtr4g 555	. . . . . 6 ⊢ (Fun ◡F → (ran F ∈ V → On ∈ V))
68	59, 67	mtoi 107	. . . . 5 ⊢ (Fun ◡F → ¬ ran F ∈ V)
69	58, 68	syl6 22	. . . 4 ⊢ ((R Po A ⋀ w We A) → (∀x(x ∈ On → D ≠ ∅) → ¬ ran F ∈ V))
70	33, 69	jcad 602	. . 3 ⊢ ((R Po A ⋀ w We A) → (∀x(x ∈ On → D ≠ ∅) → (ran F ∈ V ⋀ ¬ ran F ∈ V)))
71		df-ne 1590	. . . . 5 ⊢ (D ≠ ∅ ↔ ¬ D = ∅)
72	71	ralbii 1670	. . . 4 ⊢ (∀x ∈ On D ≠ ∅ ↔ ∀x ∈ On ¬ D = ∅)
73		df-ral 1652	. . . 4 ⊢ (∀x ∈ On D ≠ ∅ ↔ ∀x(x ∈ On → D ≠ ∅))
74		ralnex 1656	. . . 4 ⊢ (∀x ∈ On ¬ D = ∅ ↔ ¬ ∃x ∈ On D = ∅)
75	72, 73, 74	3bitr3 181	. . 3 ⊢ (∀x(x ∈ On → D ≠ ∅) ↔ ¬ ∃x ∈ On D = ∅)
76	70, 75	syl5ibr 207	. 2 ⊢ ((R Po A ⋀ w We A) → (¬ ∃x ∈ On D = ∅ → (ran F ∈ V ⋀ ¬ ran F ∈ V)))
77	1, 76	mt3i 113	1 ⊢ ((R Po A ⋀ w We A) → ∃x ∈ On D = ∅)

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 956   = wceq 958   ∈ wcel 960  {cab 1466   ≠ wne 1588  ∀wral 1648  ∃wrex 1649  {crab 1651  Vcvv 1814   ⊆ wss 2050  ∅c0 2283  ∪cuni 2507   class class class wbr 2624  {copab 2671   Po wpo 2844   We wwe 2922  Oncon0 2954  ^◡ccnv 3175  dom cdm 3176  ran crn 3177   ↾ cres 3178   “ cima 3179  Rel wrel 3181  Fun wfun 3182   Fn wfn 3183   ‘cfv 3188

This theorem is referenced by:  zorn2lem7 4804

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-suc 2960  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-f1 3201  df-fv 3204

Copyright terms: Public domain