Description: Natural numbers are finite sets. (Contributed by Stefan O'Rear, 21-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | nnfi | ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onfin2 | ⊢ ω = ( On ∩ Fin ) | |
2 | inss2 | ⊢ ( On ∩ Fin ) ⊆ Fin | |
3 | 1 2 | eqsstri | ⊢ ω ⊆ Fin |
4 | 3 | sseli | ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ Fin ) |