Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets
nnfi
Next ⟩
nndomo
Metamath Proof Explorer
Ascii
Unicode
Theorem
nnfi
Description:
Natural numbers are finite sets.
(Contributed by
Stefan O'Rear
, 21-Mar-2015)
Ref
Expression
Assertion
nnfi
⊢
A
∈
ω
→
A
∈
Fin
Proof
Step
Hyp
Ref
Expression
1
onfin2
⊢
ω
=
On
∩
Fin
2
inss2
⊢
On
∩
Fin
⊆
Fin
3
1
2
eqsstri
⊢
ω
⊆
Fin
4
3
sseli
⊢
A
∈
ω
→
A
∈
Fin