Description: The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | cardsucinf | ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( card ‘ suc 𝐴 ) = ( card ‘ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | infensuc | ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → 𝐴 ≈ suc 𝐴 ) | |
2 | carden2b | ⊢ ( 𝐴 ≈ suc 𝐴 → ( card ‘ 𝐴 ) = ( card ‘ suc 𝐴 ) ) | |
3 | 1 2 | syl | ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( card ‘ 𝐴 ) = ( card ‘ suc 𝐴 ) ) |
4 | 3 | eqcomd | ⊢ ( ( 𝐴 ∈ On ∧ ω ⊆ 𝐴 ) → ( card ‘ suc 𝐴 ) = ( card ‘ 𝐴 ) ) |