Theorem finnum

Description: Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	finnum	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		isfi	⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2		nnon	⊢ ( 𝑥 ∈ ω → 𝑥 ∈ On )
3		ensym	⊢ ( 𝐴 ≈ 𝑥 → 𝑥 ≈ 𝐴 )
4		isnumi	⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) → 𝐴 ∈ dom card )
5	2 3 4	syl2an	⊢ ( ( 𝑥 ∈ ω ∧ 𝐴 ≈ 𝑥 ) → 𝐴 ∈ dom card )
6	5	rexlimiva	⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → 𝐴 ∈ dom card )
7	1 6	sylbi	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )