Theorem onenon

Description: Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	onenon	⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		enrefg	⊢ ( 𝐴 ∈ On → 𝐴 ≈ 𝐴 )
2		isnumi	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≈ 𝐴 ) → 𝐴 ∈ dom card )
3	1 2	mpdan	⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card )