Theorem alephfp 10023

Description: The aleph function has a fixed point. Similar to Proposition 11.18 of [TakeutiZaring] p. 104, except that we construct an actual example of a fixed point rather than just showing its existence. See alephfp2 10024 for an abbreviated version just showing existence. (Contributed by NM, 6-Nov-2004.) (Proof shortened by Mario Carneiro, 15-May-2015.)

Hypothesis

Ref	Expression
alephfplem.1	⊢ 𝐻 = (rec(ℵ, ω) ↾ ω)

Assertion

Ref	Expression
alephfp	⊢ (ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω)

Proof of Theorem alephfp

Dummy variables 𝑧 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		alephfplem.1	. . 3 ⊢ 𝐻 = (rec(ℵ, ω) ↾ ω)
2	1	alephfplem4 10022	. 2 ⊢ ∪ (𝐻 “ ω) ∈ ran ℵ
3		isinfcard 10007	. . 3 ⊢ ((ω ⊆ ∪ (𝐻 “ ω) ∧ (card‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω)) ↔ ∪ (𝐻 “ ω) ∈ ran ℵ)
4		cardalephex 10005	. . . 4 ⊢ (ω ⊆ ∪ (𝐻 “ ω) → ((card‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω) ↔ ∃𝑧 ∈ On ∪ (𝐻 “ ω) = (ℵ‘𝑧)))
5	4	biimpa 476	. . 3 ⊢ ((ω ⊆ ∪ (𝐻 “ ω) ∧ (card‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω)) → ∃𝑧 ∈ On ∪ (𝐻 “ ω) = (ℵ‘𝑧))
6	3, 5	sylbir 235	. 2 ⊢ (∪ (𝐻 “ ω) ∈ ran ℵ → ∃𝑧 ∈ On ∪ (𝐻 “ ω) = (ℵ‘𝑧))
7		alephle 10003	. . . . . . . . 9 ⊢ (𝑧 ∈ On → 𝑧 ⊆ (ℵ‘𝑧))
8		alephon 9984	. . . . . . . . . . 11 ⊢ (ℵ‘𝑧) ∈ On
9	8	onirri 6432	. . . . . . . . . 10 ⊢ ¬ (ℵ‘𝑧) ∈ (ℵ‘𝑧)
10		frfnom 8369	. . . . . . . . . . . . . 14 ⊢ (rec(ℵ, ω) ↾ ω) Fn ω
11	1	fneq1i 6590	. . . . . . . . . . . . . 14 ⊢ (𝐻 Fn ω ↔ (rec(ℵ, ω) ↾ ω) Fn ω)
12	10, 11	mpbir 231	. . . . . . . . . . . . 13 ⊢ 𝐻 Fn ω
13		fnfun 6593	. . . . . . . . . . . . 13 ⊢ (𝐻 Fn ω → Fun 𝐻)
14		eluniima 7199	. . . . . . . . . . . . 13 ⊢ (Fun 𝐻 → (𝑧 ∈ ∪ (𝐻 “ ω) ↔ ∃𝑣 ∈ ω 𝑧 ∈ (𝐻‘𝑣)))
15	12, 13, 14	mp2b 10	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ∪ (𝐻 “ ω) ↔ ∃𝑣 ∈ ω 𝑧 ∈ (𝐻‘𝑣))
16		alephsson 10015	. . . . . . . . . . . . . . . 16 ⊢ ran ℵ ⊆ On
17	1	alephfplem3 10021	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ω → (𝐻‘𝑣) ∈ ran ℵ)
18	16, 17	sselid 3932	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (𝐻‘𝑣) ∈ On)
19		alephord2i 9992	. . . . . . . . . . . . . . 15 ⊢ ((𝐻‘𝑣) ∈ On → (𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ (ℵ‘(𝐻‘𝑣))))
20	18, 19	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ω → (𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ (ℵ‘(𝐻‘𝑣))))
21	1	alephfplem2 10020	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → (𝐻‘suc 𝑣) = (ℵ‘(𝐻‘𝑣)))
22		peano2 7835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ ω → suc 𝑣 ∈ ω)
23		fnfvelrn 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐻 Fn ω ∧ suc 𝑣 ∈ ω) → (𝐻‘suc 𝑣) ∈ ran 𝐻)
24	12, 23	mpan 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (suc 𝑣 ∈ ω → (𝐻‘suc 𝑣) ∈ ran 𝐻)
25		fnima 6623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐻 Fn ω → (𝐻 “ ω) = ran 𝐻)
26	12, 25	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 “ ω) = ran 𝐻
27	24, 26	eleqtrrdi 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑣 ∈ ω → (𝐻‘suc 𝑣) ∈ (𝐻 “ ω))
28	22, 27	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ ω → (𝐻‘suc 𝑣) ∈ (𝐻 “ ω))
29	21, 28	eqeltrrd 2838	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 ∈ ω → (ℵ‘(𝐻‘𝑣)) ∈ (𝐻 “ ω))
30		elssuni 4895	. . . . . . . . . . . . . . . 16 ⊢ ((ℵ‘(𝐻‘𝑣)) ∈ (𝐻 “ ω) → (ℵ‘(𝐻‘𝑣)) ⊆ ∪ (𝐻 “ ω))
31	29, 30	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑣 ∈ ω → (ℵ‘(𝐻‘𝑣)) ⊆ ∪ (𝐻 “ ω))
32	31	sseld 3933	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ ω → ((ℵ‘𝑧) ∈ (ℵ‘(𝐻‘𝑣)) → (ℵ‘𝑧) ∈ ∪ (𝐻 “ ω)))
33	20, 32	syld 47	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ ω → (𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ ∪ (𝐻 “ ω)))
34	33	rexlimiv 3131	. . . . . . . . . . . 12 ⊢ (∃𝑣 ∈ ω 𝑧 ∈ (𝐻‘𝑣) → (ℵ‘𝑧) ∈ ∪ (𝐻 “ ω))
35	15, 34	sylbi 217	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ∪ (𝐻 “ ω) → (ℵ‘𝑧) ∈ ∪ (𝐻 “ ω))
36		eleq2 2826	. . . . . . . . . . . 12 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → (𝑧 ∈ ∪ (𝐻 “ ω) ↔ 𝑧 ∈ (ℵ‘𝑧)))
37		eleq2 2826	. . . . . . . . . . . 12 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → ((ℵ‘𝑧) ∈ ∪ (𝐻 “ ω) ↔ (ℵ‘𝑧) ∈ (ℵ‘𝑧)))
38	36, 37	imbi12d 344	. . . . . . . . . . 11 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → ((𝑧 ∈ ∪ (𝐻 “ ω) → (ℵ‘𝑧) ∈ ∪ (𝐻 “ ω)) ↔ (𝑧 ∈ (ℵ‘𝑧) → (ℵ‘𝑧) ∈ (ℵ‘𝑧))))
39	35, 38	mpbii 233	. . . . . . . . . 10 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → (𝑧 ∈ (ℵ‘𝑧) → (ℵ‘𝑧) ∈ (ℵ‘𝑧)))
40	9, 39	mtoi 199	. . . . . . . . 9 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → ¬ 𝑧 ∈ (ℵ‘𝑧))
41	7, 40	anim12i 614	. . . . . . . 8 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧)))
42		eloni 6328	. . . . . . . . . 10 ⊢ (𝑧 ∈ On → Ord 𝑧)
43	8	onordi 6431	. . . . . . . . . 10 ⊢ Ord (ℵ‘𝑧)
44		ordtri4 6355	. . . . . . . . . 10 ⊢ ((Ord 𝑧 ∧ Ord (ℵ‘𝑧)) → (𝑧 = (ℵ‘𝑧) ↔ (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧))))
45	42, 43, 44	sylancl 587	. . . . . . . . 9 ⊢ (𝑧 ∈ On → (𝑧 = (ℵ‘𝑧) ↔ (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧))))
46	45	adantr 480	. . . . . . . 8 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → (𝑧 = (ℵ‘𝑧) ↔ (𝑧 ⊆ (ℵ‘𝑧) ∧ ¬ 𝑧 ∈ (ℵ‘𝑧))))
47	41, 46	mpbird 257	. . . . . . 7 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → 𝑧 = (ℵ‘𝑧))
48		eqeq2 2749	. . . . . . . 8 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → (𝑧 = ∪ (𝐻 “ ω) ↔ 𝑧 = (ℵ‘𝑧)))
49	48	adantl 481	. . . . . . 7 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → (𝑧 = ∪ (𝐻 “ ω) ↔ 𝑧 = (ℵ‘𝑧)))
50	47, 49	mpbird 257	. . . . . 6 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → 𝑧 = ∪ (𝐻 “ ω))
51	50	eqcomd 2743	. . . . 5 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → ∪ (𝐻 “ ω) = 𝑧)
52	51	fveq2d 6839	. . . 4 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → (ℵ‘∪ (𝐻 “ ω)) = (ℵ‘𝑧))
53		eqeq2 2749	. . . . 5 ⊢ (∪ (𝐻 “ ω) = (ℵ‘𝑧) → ((ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω) ↔ (ℵ‘∪ (𝐻 “ ω)) = (ℵ‘𝑧)))
54	53	adantl 481	. . . 4 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → ((ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω) ↔ (ℵ‘∪ (𝐻 “ ω)) = (ℵ‘𝑧)))
55	52, 54	mpbird 257	. . 3 ⊢ ((𝑧 ∈ On ∧ ∪ (𝐻 “ ω) = (ℵ‘𝑧)) → (ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω))
56	55	rexlimiva 3130	. 2 ⊢ (∃𝑧 ∈ On ∪ (𝐻 “ ω) = (ℵ‘𝑧) → (ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω))
57	2, 6, 56	mp2b 10	1 ⊢ (ℵ‘∪ (𝐻 “ ω)) = ∪ (𝐻 “ ω)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃wrex 3061   ⊆ wss 3902  ∪ cuni 4864  ran crn 5626   ↾ cres 5627   “ cima 5628  Ord word 6317  Oncon0 6318  suc csuc 6320  Fun wfun 6487   Fn wfn 6488  ‘cfv 6493  ωcom 7811  reccrdg 8343  cardccrd 9852  ℵcale 9853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683  ax-inf2 9555

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-om 7812  df-2nd 7937  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-1o 8400  df-er 8638  df-en 8889  df-dom 8890  df-sdom 8891  df-fin 8892  df-oi 9420  df-har 9467  df-card 9856  df-aleph 9857

This theorem is referenced by:  alephfp2  10024