This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephfp

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 for an abbreviated version just showing existence. (Contributed by NM, 6-Nov-2004) (Proof shortened by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis alephfplem.1 ⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
Assertion alephfp ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω )

Proof

Step Hyp Ref Expression
1 alephfplem.1 ⊢ 𝐻 = ( rec ( ℵ , ω ) ↾ ω )
2 1 alephfplem4 ⊢ ∪ ( 𝐻 “ ω ) ∈ ran ℵ
3 isinfcard ⊢ ( ( ω ⊆ ∪ ( 𝐻 “ ω ) ∧ ( card ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) ) ↔ ∪ ( 𝐻 “ ω ) ∈ ran ℵ )
4 cardalephex ⊢ ( ω ⊆ ∪ ( 𝐻 “ ω ) → ( ( card ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) ↔ ∃ 𝑧 ∈ On ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) )
5 4 biimpa ⊢ ( ( ω ⊆ ∪ ( 𝐻 “ ω ) ∧ ( card ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) ) → ∃ 𝑧 ∈ On ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) )
6 3 5 sylbir ⊢ ( ∪ ( 𝐻 “ ω ) ∈ ran ℵ → ∃ 𝑧 ∈ On ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) )
7 alephle ⊢ ( 𝑧 ∈ On → 𝑧 ⊆ ( ℵ ‘ 𝑧 ) )
8 alephon ⊢ ( ℵ ‘ 𝑧 ) ∈ On
9 8 onirri ⊢ ¬ ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ 𝑧 )
10 frfnom ⊢ ( rec ( ℵ , ω ) ↾ ω ) Fn ω
11 1 fneq1i ⊢ ( 𝐻 Fn ω ↔ ( rec ( ℵ , ω ) ↾ ω ) Fn ω )
12 10 11 mpbir ⊢ 𝐻 Fn ω
13 fnfun ⊢ ( 𝐻 Fn ω → Fun 𝐻 )
14 eluniima ⊢ ( Fun 𝐻 → ( 𝑧 ∈ ∪ ( 𝐻 “ ω ) ↔ ∃ 𝑣 ∈ ω 𝑧 ∈ ( 𝐻 ‘ 𝑣 ) ) )
15 12 13 14 mp2b ⊢ ( 𝑧 ∈ ∪ ( 𝐻 “ ω ) ↔ ∃ 𝑣 ∈ ω 𝑧 ∈ ( 𝐻 ‘ 𝑣 ) )
16 alephsson ⊢ ran ℵ ⊆ On
17 1 alephfplem3 ⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ 𝑣 ) ∈ ran ℵ )
18 16 17 sselid ⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ 𝑣 ) ∈ On )
19 alephord2i ⊢ ( ( 𝐻 ‘ 𝑣 ) ∈ On → ( 𝑧 ∈ ( 𝐻 ‘ 𝑣 ) → ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
20 18 19 syl ⊢ ( 𝑣 ∈ ω → ( 𝑧 ∈ ( 𝐻 ‘ 𝑣 ) → ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) ) )
21 1 alephfplem2 ⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ suc 𝑣 ) = ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) )
22 peano2 ⊢ ( 𝑣 ∈ ω → suc 𝑣 ∈ ω )
23 fnfvelrn ⊢ ( ( 𝐻 Fn ω ∧ suc 𝑣 ∈ ω ) → ( 𝐻 ‘ suc 𝑣 ) ∈ ran 𝐻 )
24 12 23 mpan ⊢ ( suc 𝑣 ∈ ω → ( 𝐻 ‘ suc 𝑣 ) ∈ ran 𝐻 )
25 fnima ⊢ ( 𝐻 Fn ω → ( 𝐻 “ ω ) = ran 𝐻 )
26 12 25 ax-mp ⊢ ( 𝐻 “ ω ) = ran 𝐻
27 24 26 eleqtrrdi ⊢ ( suc 𝑣 ∈ ω → ( 𝐻 ‘ suc 𝑣 ) ∈ ( 𝐻 “ ω ) )
28 22 27 syl ⊢ ( 𝑣 ∈ ω → ( 𝐻 ‘ suc 𝑣 ) ∈ ( 𝐻 “ ω ) )
29 21 28 eqeltrrd ⊢ ( 𝑣 ∈ ω → ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐻 “ ω ) )
30 elssuni ⊢ ( ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) ∈ ( 𝐻 “ ω ) → ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) ⊆ ∪ ( 𝐻 “ ω ) )
31 29 30 syl ⊢ ( 𝑣 ∈ ω → ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) ⊆ ∪ ( 𝐻 “ ω ) )
32 31 sseld ⊢ ( 𝑣 ∈ ω → ( ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ ( 𝐻 ‘ 𝑣 ) ) → ( ℵ ‘ 𝑧 ) ∈ ∪ ( 𝐻 “ ω ) ) )
33 20 32 syld ⊢ ( 𝑣 ∈ ω → ( 𝑧 ∈ ( 𝐻 ‘ 𝑣 ) → ( ℵ ‘ 𝑧 ) ∈ ∪ ( 𝐻 “ ω ) ) )
34 33 rexlimiv ⊢ ( ∃ 𝑣 ∈ ω 𝑧 ∈ ( 𝐻 ‘ 𝑣 ) → ( ℵ ‘ 𝑧 ) ∈ ∪ ( 𝐻 “ ω ) )
35 15 34 sylbi ⊢ ( 𝑧 ∈ ∪ ( 𝐻 “ ω ) → ( ℵ ‘ 𝑧 ) ∈ ∪ ( 𝐻 “ ω ) )
36 eleq2 ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( 𝑧 ∈ ∪ ( 𝐻 “ ω ) ↔ 𝑧 ∈ ( ℵ ‘ 𝑧 ) ) )
37 eleq2 ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( ( ℵ ‘ 𝑧 ) ∈ ∪ ( 𝐻 “ ω ) ↔ ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ 𝑧 ) ) )
38 36 37 imbi12d ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( ( 𝑧 ∈ ∪ ( 𝐻 “ ω ) → ( ℵ ‘ 𝑧 ) ∈ ∪ ( 𝐻 “ ω ) ) ↔ ( 𝑧 ∈ ( ℵ ‘ 𝑧 ) → ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ 𝑧 ) ) ) )
39 35 38 mpbii ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( 𝑧 ∈ ( ℵ ‘ 𝑧 ) → ( ℵ ‘ 𝑧 ) ∈ ( ℵ ‘ 𝑧 ) ) )
40 9 39 mtoi ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ¬ 𝑧 ∈ ( ℵ ‘ 𝑧 ) )
41 7 40 anim12i ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ( 𝑧 ⊆ ( ℵ ‘ 𝑧 ) ∧ ¬ 𝑧 ∈ ( ℵ ‘ 𝑧 ) ) )
42 eloni ⊢ ( 𝑧 ∈ On → Ord 𝑧 )
43 8 onordi ⊢ Ord ( ℵ ‘ 𝑧 )
44 ordtri4 ⊢ ( ( Ord 𝑧 ∧ Ord ( ℵ ‘ 𝑧 ) ) → ( 𝑧 = ( ℵ ‘ 𝑧 ) ↔ ( 𝑧 ⊆ ( ℵ ‘ 𝑧 ) ∧ ¬ 𝑧 ∈ ( ℵ ‘ 𝑧 ) ) ) )
45 42 43 44 sylancl ⊢ ( 𝑧 ∈ On → ( 𝑧 = ( ℵ ‘ 𝑧 ) ↔ ( 𝑧 ⊆ ( ℵ ‘ 𝑧 ) ∧ ¬ 𝑧 ∈ ( ℵ ‘ 𝑧 ) ) ) )
46 45 adantr ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ( 𝑧 = ( ℵ ‘ 𝑧 ) ↔ ( 𝑧 ⊆ ( ℵ ‘ 𝑧 ) ∧ ¬ 𝑧 ∈ ( ℵ ‘ 𝑧 ) ) ) )
47 41 46 mpbird ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → 𝑧 = ( ℵ ‘ 𝑧 ) )
48 eqeq2 ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( 𝑧 = ∪ ( 𝐻 “ ω ) ↔ 𝑧 = ( ℵ ‘ 𝑧 ) ) )
49 48 adantl ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ( 𝑧 = ∪ ( 𝐻 “ ω ) ↔ 𝑧 = ( ℵ ‘ 𝑧 ) ) )
50 47 49 mpbird ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → 𝑧 = ∪ ( 𝐻 “ ω ) )
51 50 eqcomd ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ∪ ( 𝐻 “ ω ) = 𝑧 )
52 51 fveq2d ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ( ℵ ‘ 𝑧 ) )
53 eqeq2 ⊢ ( ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) ↔ ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ( ℵ ‘ 𝑧 ) ) )
54 53 adantl ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ( ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) ↔ ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ( ℵ ‘ 𝑧 ) ) )
55 52 54 mpbird ⊢ ( ( 𝑧 ∈ On ∧ ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) ) → ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) )
56 55 rexlimiva ⊢ ( ∃ 𝑧 ∈ On ∪ ( 𝐻 “ ω ) = ( ℵ ‘ 𝑧 ) → ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω ) )
57 2 6 56 mp2b ⊢ ( ℵ ‘ ∪ ( 𝐻 “ ω ) ) = ∪ ( 𝐻 “ ω )