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

Metamath Proof Explorer

Theorem cardnn

Description: The cardinality of a natural number is the number. Corollary 10.23 of TakeutiZaring p. 90. (Contributed by Mario Carneiro, 7-Jan-2013)

Ref Expression
Assertion cardnn ⊢ A ∈ ω → card ⁡ A = A

Proof

Step Hyp Ref Expression
1 nnon ⊢ A ∈ ω → A ∈ On
2 onenon ⊢ A ∈ On → A ∈ dom ⁡ card
3 cardid2 ⊢ A ∈ dom ⁡ card → card ⁡ A ≈ A
4 1 2 3 3syl ⊢ A ∈ ω → card ⁡ A ≈ A
5 nnfi ⊢ A ∈ ω → A ∈ Fin
6 ficardom ⊢ A ∈ Fin → card ⁡ A ∈ ω
7 5 6 syl ⊢ A ∈ ω → card ⁡ A ∈ ω
8 nneneq ⊢ card ⁡ A ∈ ω ∧ A ∈ ω → card ⁡ A ≈ A ↔ card ⁡ A = A
9 7 8 mpancom ⊢ A ∈ ω → card ⁡ A ≈ A ↔ card ⁡ A = A
10 4 9 mpbid ⊢ A ∈ ω → card ⁡ A = A