Theorem nnfiOLD

Description: Obsolete version of nnfi as of 23-Sep-2024. (Contributed by Stefan O'Rear, 21-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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