Metamath Proof Explorer


Theorem cardalephex

Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)

Ref Expression
Assertion cardalephex ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ω ⊆ 𝐴 )
2 cardaleph ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → 𝐴 = ( ℵ ‘ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) )
3 2 sseq2d ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( ω ⊆ 𝐴 ↔ ω ⊆ ( ℵ ‘ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) ) )
4 alephgeom ( { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On ↔ ω ⊆ ( ℵ ‘ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) )
5 3 4 bitr4di ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ( ω ⊆ 𝐴 { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On ) )
6 1 5 mpbid ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On )
7 fveq2 ( 𝑥 = { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) )
8 7 rspceeqv ( ( { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ∈ On ∧ 𝐴 = ( ℵ ‘ { 𝑦 ∈ On ∣ 𝐴 ⊆ ( ℵ ‘ 𝑦 ) } ) ) → ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) )
9 6 2 8 syl2anc ( ( ω ⊆ 𝐴 ∧ ( card ‘ 𝐴 ) = 𝐴 ) → ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) )
10 9 ex ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 → ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )
11 alephcard ( card ‘ ( ℵ ‘ 𝑥 ) ) = ( ℵ ‘ 𝑥 )
12 fveq2 ( 𝐴 = ( ℵ ‘ 𝑥 ) → ( card ‘ 𝐴 ) = ( card ‘ ( ℵ ‘ 𝑥 ) ) )
13 id ( 𝐴 = ( ℵ ‘ 𝑥 ) → 𝐴 = ( ℵ ‘ 𝑥 ) )
14 11 12 13 3eqtr4a ( 𝐴 = ( ℵ ‘ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
15 14 rexlimivw ( ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) → ( card ‘ 𝐴 ) = 𝐴 )
16 10 15 impbid1 ( ω ⊆ 𝐴 → ( ( card ‘ 𝐴 ) = 𝐴 ↔ ∃ 𝑥 ∈ On 𝐴 = ( ℵ ‘ 𝑥 ) ) )