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	⊢ ( 𝐴 ∈ ω → ( card ‘ 𝐴 ) = 𝐴 )

Proof

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