Theorem nnfi

Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Assertion	nnfi	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		onfin2	⊢ ω = ( On ∩ Fin )
2		inss2	⊢ ( On ∩ Fin ) ⊆ Fin
3	1 2	eqsstri	⊢ ω ⊆ Fin
4	3	sseli	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin )