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

Metamath Proof Explorer

Theorem alephcard

Description: Every aleph is a cardinal number. Theorem 65 of Suppes p. 229. (Contributed by NM, 25-Oct-2003) (Revised by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephcard ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 2fveq3 ⊢ ( 𝑥 = ∅ → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ ∅ ) ) )
2 fveq2 ⊢ ( 𝑥 = ∅ → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ ∅ ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ ∅ ) ) = ( ℵ ‘ ∅ ) ) )
4 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ 𝑦 ) ) )
5 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) )
6 4 5 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) )
7 2fveq3 ⊢ ( 𝑥 = suc 𝑦 → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ suc 𝑦 ) ) )
8 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ suc 𝑦 ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( ℵ ‘ suc 𝑦 ) ) )
10 2fveq3 ⊢ ( 𝑥 = 𝐴 → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ( ℵ ‘ 𝐴 ) ) )
11 fveq2 ⊢ ( 𝑥 = 𝐴 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ↔ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) ) )
13 cardom ⊢ ( card ‘ ω ) = ω
14 aleph0 ⊢ ( ℵ ‘ ∅ ) = ω
15 14 fveq2i ⊢ ( card ‘ ( ℵ ‘ ∅ ) ) = ( card ‘ ω )
16 13 15 14 3eqtr4i ⊢ ( card ‘ ( ℵ ‘ ∅ ) ) = ( ℵ ‘ ∅ )
17 harcard ⊢ ( card ‘ ( har ‘ ( ℵ ‘ 𝑦 ) ) ) = ( har ‘ ( ℵ ‘ 𝑦 ) )
18 alephsuc ⊢ ( 𝑦 ∈ On → ( ℵ ‘ suc 𝑦 ) = ( har ‘ ( ℵ ‘ 𝑦 ) ) )
19 18 fveq2d ⊢ ( 𝑦 ∈ On → ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( card ‘ ( har ‘ ( ℵ ‘ 𝑦 ) ) ) )
20 17 19 18 3eqtr4a ⊢ ( 𝑦 ∈ On → ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( ℵ ‘ suc 𝑦 ) )
21 20 a1d ⊢ ( 𝑦 ∈ On → ( ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ( ℵ ‘ suc 𝑦 ) ) = ( ℵ ‘ suc 𝑦 ) ) )
22 cardiun ⊢ ( 𝑥 ∈ V → ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) )
23 22 elv ⊢ ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
24 23 adantl ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
25 vex ⊢ 𝑥 ∈ V
26 alephlim ⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( ℵ ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
27 25 26 mpan ⊢ ( Lim 𝑥 → ( ℵ ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
28 27 adantr ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( ℵ ‘ 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) )
29 28 fveq2d ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( card ‘ ∪ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ) )
30 24 29 28 3eqtr4d ⊢ ( ( Lim 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) ) → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) )
31 30 ex ⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( card ‘ ( ℵ ‘ 𝑦 ) ) = ( ℵ ‘ 𝑦 ) → ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 ) ) )
32 3 6 9 12 16 21 31 tfinds ⊢ ( 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
33 card0 ⊢ ( card ‘ ∅ ) = ∅
34 alephfnon ⊢ ℵ Fn On
35 34 fndmi ⊢ dom ℵ = On
36 35 eleq2i ⊢ ( 𝐴 ∈ dom ℵ ↔ 𝐴 ∈ On )
37 ndmfv ⊢ ( ¬ 𝐴 ∈ dom ℵ → ( ℵ ‘ 𝐴 ) = ∅ )
38 36 37 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = ∅ )
39 38 fveq2d ⊢ ( ¬ 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( card ‘ ∅ ) )
40 33 39 38 3eqtr4a ⊢ ( ¬ 𝐴 ∈ On → ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) )
41 32 40 pm2.61i ⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )