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

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 𝐴 = ( ℵ ‘ 𝑥 ) ) )