Theorem zornlem1 3603

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
zornlem1	⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → (F ‘x) ∈ 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 zornlem1

Step	Hyp	Ref	Expression
1		zornlem.2	. . . . . 6 ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}
2		zornlem.3	. . . . . 6 ⊢ F = ∪B
3	1, 2	tfr2 2963	. . . . 5 ⊢ (x ∈ On → (F ‘x) = (G ‘(F ↾ x)))
4		zornlem.6	. . . . . . 7 ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}
5	4	fveq1i 2833	. . . . . 6 ⊢ (G ‘(F ↾ x)) = ({⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}} ‘(F ↾ x))
6		visset 1350	. . . . . . . 8 ⊢ x ∈ V
7	1, 2	tfrlem7 2955	. . . . . . . 8 ⊢ Fun F
8		resfunexg 2717	. . . . . . . 8 ⊢ (x ∈ V → (Fun F → (F ↾ x) ∈ V))
9	6, 7, 8	mp2 43	. . . . . . 7 ⊢ (F ↾ x) ∈ V
10		zornlem.1	. . . . . . . . . 10 ⊢ A ∈ V
11		zornlem.5	. . . . . . . . . . 11 ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}
12		ssrab 1556	. . . . . . . . . . 11 ⊢ {z ∈ A∣∀g ∈ (F “ x)gRz} ⊆ A
13	11, 12	eqsstr 1530	. . . . . . . . . 10 ⊢ D ⊆ A
14	10, 13	ssexi 1701	. . . . . . . . 9 ⊢ D ∈ V
15	14	rabex 1706	. . . . . . . 8 ⊢ {v ∈ D∣∀u ∈ D ¬ uwv} ∈ V
16	15	uniex 1947	. . . . . . 7 ⊢ ∪{v ∈ D∣∀u ∈ D ¬ uwv} ∈ V
17		rneq 2555	. . . . . . . . . . . . . . . . . 18 ⊢ (f = (F ↾ x) → ran f = ran (F ↾ x))
18		df-ima 2431	. . . . . . . . . . . . . . . . . 18 ⊢ (F “ x) = ran (F ↾ x)
19	17, 18	syl6eqr 1142	. . . . . . . . . . . . . . . . 17 ⊢ (f = (F ↾ x) → ran f = (F “ x))
20	19	eleq2d 1156	. . . . . . . . . . . . . . . 16 ⊢ (f = (F ↾ x) → (g ∈ ran f ↔ g ∈ (F “ x)))
21	20	imbi1d 465	. . . . . . . . . . . . . . 15 ⊢ (f = (F ↾ x) → ((g ∈ ran f → gRz) ↔ (g ∈ (F “ x) → gRz)))
22	21	biraldv2 1221	. . . . . . . . . . . . . 14 ⊢ (f = (F ↾ x) → (∀g ∈ ran fgRz ↔ ∀g ∈ (F “ x)gRz))
23	22	birabsdv 1344	. . . . . . . . . . . . 13 ⊢ (f = (F ↾ x) → {z ∈ A∣∀g ∈ ran fgRz} = {z ∈ A∣∀g ∈ (F “ x)gRz})
24		zornlem.4	. . . . . . . . . . . . 13 ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}
25	23, 24, 11	3eqtr4g 1147	. . . . . . . . . . . 12 ⊢ (f = (F ↾ x) → C = D)
26	25	eleq2d 1156	. . . . . . . . . . 11 ⊢ (f = (F ↾ x) → (v ∈ C ↔ v ∈ D))
27	25	eleq2d 1156	. . . . . . . . . . . . 13 ⊢ (f = (F ↾ x) → (u ∈ C ↔ u ∈ D))
28	27	imbi1d 465	. . . . . . . . . . . 12 ⊢ (f = (F ↾ x) → ((u ∈ C → ¬ uwv) ↔ (u ∈ D → ¬ uwv)))
29	28	biraldv2 1221	. . . . . . . . . . 11 ⊢ (f = (F ↾ x) → (∀u ∈ C ¬ uwv ↔ ∀u ∈ D ¬ uwv))
30	26, 29	anbi12d 476	. . . . . . . . . 10 ⊢ (f = (F ↾ x) → ((v ∈ C ∧ ∀u ∈ C ¬ uwv) ↔ (v ∈ D ∧ ∀u ∈ D ¬ uwv)))
31	30	biabdv 1183	. . . . . . . . 9 ⊢ (f = (F ↾ x) → {v∣(v ∈ C ∧ ∀u ∈ C ¬ uwv)} = {v∣(v ∈ D ∧ ∀u ∈ D ¬ uwv)})
32		df-rab 1208	. . . . . . . . 9 ⊢ {v ∈ C∣∀u ∈ C ¬ uwv} = {v∣(v ∈ C ∧ ∀u ∈ C ¬ uwv)}
33		df-rab 1208	. . . . . . . . 9 ⊢ {v ∈ D∣∀u ∈ D ¬ uwv} = {v∣(v ∈ D ∧ ∀u ∈ D ¬ uwv)}
34	31, 32, 33	3eqtr4g 1147	. . . . . . . 8 ⊢ (f = (F ↾ x) → {v ∈ C∣∀u ∈ C ¬ uwv} = {v ∈ D∣∀u ∈ D ¬ uwv})
35	34	unieqd 1929	. . . . . . 7 ⊢ (f = (F ↾ x) → ∪{v ∈ C∣∀u ∈ C ¬ uwv} = ∪{v ∈ D∣∀u ∈ D ¬ uwv})
36	9, 16, 35	fvopab 2877	. . . . . 6 ⊢ ({⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}} ‘(F ↾ x)) = ∪{v ∈ D∣∀u ∈ D ¬ uwv}
37	5, 36	eqtr 1119	. . . . 5 ⊢ (G ‘(F ↾ x)) = ∪{v ∈ D∣∀u ∈ D ¬ uwv}
38	3, 37	syl6eq 1140	. . . 4 ⊢ (x ∈ On → (F ‘x) = ∪{v ∈ D∣∀u ∈ D ¬ uwv})
39	38	eleq1d 1155	. . 3 ⊢ (x ∈ On → ((F ‘x) ∈ D ↔ ∪{v ∈ D∣∀u ∈ D ¬ uwv} ∈ D))
40	14	wereu 2197	. . . . 5 ⊢ ((w We A ∧ (D ⊆ A ∧ ¬ D = ∅)) → ∃!v ∈ D ∀u ∈ D ¬ uwv)
41	13, 40	mpan21 531	. . . 4 ⊢ ((w We A ∧ ¬ D = ∅) → ∃!v ∈ D ∀u ∈ D ¬ uwv)
42		reucl 1957	. . . 4 ⊢ (∃!v ∈ D ∀u ∈ D ¬ uwv → ∪{v ∈ D∣∀u ∈ D ¬ uwv} ∈ D)
43	41, 42	syl 12	. . 3 ⊢ ((w We A ∧ ¬ D = ∅) → ∪{v ∈ D∣∀u ∈ D ¬ uwv} ∈ D)
44	39, 43	syl5bir 184	. 2 ⊢ (x ∈ On → ((w We A ∧ ¬ D = ∅) → (F ‘x) ∈ D))
45	44	imp 277	1 ⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → (F ‘x) ∈ D)

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  {cab 1090   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202  ∃!wreu 1203  {crab 1204  Vcvv 1348   ⊆ wss 1487  ∅c0 1707  ∪cuni 1919   class class class wbr 2054  {copab 2055   We wwe 2062  Oncon0 2199  ran crn 2411   ↾ cres 2412   “ cima 2413  Fun wfun 2416   Fn wfn 2417   ‘cfv 2422

This theorem is referenced by:  zornlem2 3604  zornlem3 3605  zornlem4 3606  zornlem5 3607

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-fv 2438

metamath.org