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

Metamath Proof Explorer

Theorem cardsucinf

Description: The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013)

Ref Expression
Assertion cardsucinf ⊢ A ∈ On ∧ ω ⊆ A → card ⁡ suc ⁡ A = card ⁡ A

Proof

Step Hyp Ref Expression
1 infensuc ⊢ A ∈ On ∧ ω ⊆ A → A ≈ suc ⁡ A
2 carden2b ⊢ A ≈ suc ⁡ A → card ⁡ A = card ⁡ suc ⁡ A
3 1 2 syl ⊢ A ∈ On ∧ ω ⊆ A → card ⁡ A = card ⁡ suc ⁡ A
4 3 eqcomd ⊢ A ∈ On ∧ ω ⊆ A → card ⁡ suc ⁡ A = card ⁡ A