Theorem zornlem4 3606

Description: Lemma for Zorn's lemma.

Hypotheses

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

Assertion

Ref	Expression
zornlem4	⊢ ((R Po A ∧ w We A) → ∃x ∈ 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 ∈ V ∧ ¬ ran F ∈ V)
2		ax-17 925	. . . . . . . . . . . 12 ⊢ (w We A → ∀x w We A)
3		hba1 698	. . . . . . . . . . . 12 ⊢ (∀x(x ∈ On → ¬ D = ∅) → ∀x∀x(x ∈ On → ¬ D = ∅))
4	2, 3	hban 704	. . . . . . . . . . 11 ⊢ ((w We A ∧ ∀x(x ∈ On → ¬ D = ∅)) → ∀x(w We A ∧ ∀x(x ∈ On → ¬ D = ∅)))
5		ax-17 925	. . . . . . . . . . 11 ⊢ (y ∈ A → ∀x y ∈ A)
6		eleq1 1149	. . . . . . . . . . . . . . . . . 18 ⊢ ((F ‘x) = y → ((F ‘x) ∈ A ↔ y ∈ A))
7		zornlem.1	. . . . . . . . . . . . . . . . . . . 20 ⊢ A ∈ V
8		zornlem.2	. . . . . . . . . . . . . . . . . . . 20 ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
9		zornlem.3	. . . . . . . . . . . . . . . . . . . 20 ⊢ F = ∪B
10		zornlem.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}
11		zornlem.5	. . . . . . . . . . . . . . . . . . . 20 ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
12		zornlem.6	. . . . . . . . . . . . . . . . . . . 20 ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
13	7, 8, 9, 10, 11, 12	zornlem1 3603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → (F ‘x) ∈ D)
14		ssrab 1556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {z ∈ A∣∀g ∈ (F “ x)gRz} ⊆ A
15	11, 14	eqsstr 1530	. . . . . . . . . . . . . . . . . . . 20 ⊢ D ⊆ A
16	15	sseli 1504	. . . . . . . . . . . . . . . . . . 19 ⊢ ((F ‘x) ∈ D → (F ‘x) ∈ A)
17	13, 16	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → (F ‘x) ∈ A)
18	6, 17	syl5bi 183	. . . . . . . . . . . . . . . . 17 ⊢ ((F ‘x) = y → ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → y ∈ A))
19	18	com12 13	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → ((F ‘x) = y → y ∈ A))
20	19	exp32 294	. . . . . . . . . . . . . . 15 ⊢ (x ∈ On → (w We A → (¬ D = ∅ → ((F ‘x) = y → y ∈ A))))
21	20	com12 13	. . . . . . . . . . . . . 14 ⊢ (w We A → (x ∈ On → (¬ D = ∅ → ((F ‘x) = y → y ∈ A))))
22	21	a2d 15	. . . . . . . . . . . . 13 ⊢ (w We A → ((x ∈ On → ¬ D = ∅) → (x ∈ On → ((F ‘x) = y → y ∈ A))))
23	22	a4sd 683	. . . . . . . . . . . 12 ⊢ (w We A → (∀x(x ∈ On → ¬ D = ∅) → (x ∈ On → ((F ‘x) = y → y ∈ A))))
24	23	imp 277	. . . . . . . . . . 11 ⊢ ((w We A ∧ ∀x(x ∈ On → ¬ D = ∅)) → (x ∈ On → ((F ‘x) = y → y ∈ A)))
25	4, 5, 24	r19.23ad 1285	. . . . . . . . . 10 ⊢ ((w We A ∧ ∀x(x ∈ On → ¬ D = ∅)) → (∃x ∈ On (F ‘x) = y → y ∈ A))
26	8, 9	tfr1 2962	. . . . . . . . . . 11 ⊢ F Fn On
27		fvelrn 2883	. . . . . . . . . . 11 ⊢ (F Fn On → (y ∈ ran F ↔ ∃x ∈ On (F ‘x) = y))
28	26, 27	ax-mp 6	. . . . . . . . . 10 ⊢ (y ∈ ran F ↔ ∃x ∈ On (F ‘x) = y)
29	25, 28	syl5ib 181	. . . . . . . . 9 ⊢ ((w We A ∧ ∀x(x ∈ On → ¬ D = ∅)) → (y ∈ ran F → y ∈ A))
30	29	ssrdv 1509	. . . . . . . 8 ⊢ ((w We A ∧ ∀x(x ∈ On → ¬ D = ∅)) → ran F ⊆ A)
31	7	ssex 1700	. . . . . . . 8 ⊢ (ran F ⊆ A → ran F ∈ V)
32	30, 31	syl 12	. . . . . . 7 ⊢ ((w We A ∧ ∀x(x ∈ On → ¬ D = ∅)) → ran F ∈ V)
33	32	exp 291	. . . . . 6 ⊢ (w We A → (∀x(x ∈ On → ¬ D = ∅) → ran F ∈ V))
34	33	adantl 305	. . . . 5 ⊢ ((R Po A ∧ w We A) → (∀x(x ∈ On → ¬ D = ∅) → ran F ∈ V))
35	7, 8, 9, 10, 11, 12	zornlem3 3605	. . . . . . . . . . . . . . 15 ⊢ ((R Po A ∧ (x ∈ On ∧ (w We A ∧ ¬ D = ∅))) → (y ∈ x → ¬ (F ‘x) = (F ‘y)))
36	35	exp45 303	. . . . . . . . . . . . . 14 ⊢ (R Po A → (x ∈ On → (w We A → (¬ D = ∅ → (y ∈ x → ¬ (F ‘x) = (F ‘y))))))
37	36	com23 32	. . . . . . . . . . . . 13 ⊢ (R Po A → (w We A → (x ∈ On → (¬ D = ∅ → (y ∈ x → ¬ (F ‘x) = (F ‘y))))))
38	37	imp 277	. . . . . . . . . . . 12 ⊢ ((R Po A ∧ w We A) → (x ∈ On → (¬ D = ∅ → (y ∈ x → ¬ (F ‘x) = (F ‘y)))))
39	38	a2d 15	. . . . . . . . . . 11 ⊢ ((R Po A ∧ w We A) → ((x ∈ On → ¬ D = ∅) → (x ∈ On → (y ∈ x → ¬ (F ‘x) = (F ‘y)))))
40	39	imp4a 282	. . . . . . . . . 10 ⊢ ((R Po A ∧ w We A) → ((x ∈ On → ¬ D = ∅) → ((x ∈ On ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y))))
41	40	19.21adv 945	. . . . . . . . 9 ⊢ ((R Po A ∧ w We A) → ((x ∈ On → ¬ D = ∅) → ∀y((x ∈ On ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y))))
42	41	19.20dv 946	. . . . . . . 8 ⊢ ((R Po A ∧ w We A) → (∀x(x ∈ On → ¬ D = ∅) → ∀x∀y((x ∈ On ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y))))
43		r2al 1231	. . . . . . . 8 ⊢ (∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y) ↔ ∀x∀y((x ∈ On ∧ y ∈ x) → ¬ (F ‘x) = (F ‘y)))
44	42, 43	syl6ibr 186	. . . . . . 7 ⊢ ((R Po A ∧ w We A) → (∀x(x ∈ On → ¬ D = ∅) → ∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y)))
45		ssid 1519	. . . . . . . . 9 ⊢ On ⊆ On
46	26	tz7.48lem 2993	. . . . . . . . 9 ⊢ ((On ⊆ On ∧ ∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y)) → Fun ◡(F ↾ On))
47	45, 46	mpan 518	. . . . . . . 8 ⊢ (∀x ∈ On ∀y ∈ 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 ⊢ (∀x ∈ On ∀y ∈ x ¬ (F ‘x) = (F ‘y) → Fun ◡F)
59	44, 58	syl6 23	. . . . . 6 ⊢ ((R Po A ∧ w We A) → (∀x(x ∈ On → ¬ D = ∅) → Fun ◡F))
60		onprc 2240	. . . . . . 7 ⊢ ¬ On ∈ V
61		funrnex 2743	. . . . . . . . 9 ⊢ (dom ◡F ∈ V → (Fun ◡F → ran ◡F ∈ V))
62	61	com12 13	. . . . . . . 8 ⊢ (Fun ◡F → (dom ◡F ∈ V → ran ◡F ∈ V))
63		df-rn 2429	. . . . . . . . 9 ⊢ ran F = dom ◡F
64	63	eleq1i 1152	. . . . . . . 8 ⊢ (ran F ∈ V ↔ dom ◡F ∈ V)
65		dfdm4 2525	. . . . . . . . . 10 ⊢ dom F = ran ◡F
66	50, 65	eqtr3 1121	. . . . . . . . 9 ⊢ On = ran ◡F
67	66	eleq1i 1152	. . . . . . . 8 ⊢ (On ∈ V ↔ ran ◡F ∈ V)
68	62, 64, 67	3imtr4g 426	. . . . . . 7 ⊢ (Fun ◡F → (ran F ∈ V → On ∈ V))
69	60, 68	mtoi 94	. . . . . 6 ⊢ (Fun ◡F → ¬ ran F ∈ V)
70	59, 69	syl6 23	. . . . 5 ⊢ ((R Po A ∧ w We A) → (∀x(x ∈ On → ¬ D = ∅) → ¬ ran F ∈ V))
71	34, 70	jcad 455	. . . 4 ⊢ ((R Po A ∧ w We A) → (∀x(x ∈ On → ¬ D = ∅) → (ran F ∈ V ∧ ¬ ran F ∈ V)))
72		alinexa 724	. . . 4 ⊢ (∀x(x ∈ On → ¬ D = ∅) ↔ ¬ ∃x(x ∈ On ∧ D = ∅))
73	71, 72	syl5ibr 182	. . 3 ⊢ ((R Po A ∧ w We A) → (¬ ∃x(x ∈ On ∧ D = ∅) → (ran F ∈ V ∧ ¬ ran F ∈ V)))
74	1, 73	mt3i 100	. 2 ⊢ ((R Po A ∧ w We A) → ∃x(x ∈ On ∧ D = ∅))
75		df-rex 1206	. 2 ⊢ (∃x ∈ On D = ∅ ↔ ∃x(x ∈ On ∧ D = ∅))
76	74, 75	sylibr 175	1 ⊢ ((R Po A ∧ w We A) → ∃x ∈ On D = ∅)

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wel 803  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  {crab 1204  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ∪cuni 1919   class class class wbr 2054  {copab 2055   Po wpo 2058   We wwe 2062  Oncon0 2199  ^◡ccnv 2409  dom cdm 2410  ran crn 2411   ↾ cres 2412   “ cima 2413  Rel wrel 2415  Fun wfun 2416   Fn wfn 2417   ‘cfv 2422

This theorem is referenced by:  zornlem7 3609

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-suc 2205  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438

metamath.org