Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Finite sets
ssnnfi
Next ⟩
0fin
Metamath Proof Explorer
Ascii
Unicode
Theorem
ssnnfi
Description:
A subset of a natural number is finite.
(Contributed by
NM
, 24-Jun-1998)
Ref
Expression
Assertion
ssnnfi
⊢
A
∈
ω
∧
B
⊆
A
→
B
∈
Fin
Proof
Step
Hyp
Ref
Expression
1
sspss
⊢
B
⊆
A
↔
B
⊂
A
∨
B
=
A
2
pssnn
⊢
A
∈
ω
∧
B
⊂
A
→
∃
x
∈
A
B
≈
x
3
elnn
⊢
x
∈
A
∧
A
∈
ω
→
x
∈
ω
4
3
expcom
⊢
A
∈
ω
→
x
∈
A
→
x
∈
ω
5
4
anim1d
⊢
A
∈
ω
→
x
∈
A
∧
B
≈
x
→
x
∈
ω
∧
B
≈
x
6
5
reximdv2
⊢
A
∈
ω
→
∃
x
∈
A
B
≈
x
→
∃
x
∈
ω
B
≈
x
7
6
adantr
⊢
A
∈
ω
∧
B
⊂
A
→
∃
x
∈
A
B
≈
x
→
∃
x
∈
ω
B
≈
x
8
2
7
mpd
⊢
A
∈
ω
∧
B
⊂
A
→
∃
x
∈
ω
B
≈
x
9
eleq1
⊢
B
=
A
→
B
∈
ω
↔
A
∈
ω
10
9
biimparc
⊢
A
∈
ω
∧
B
=
A
→
B
∈
ω
11
enrefnn
⊢
B
∈
ω
→
B
≈
B
12
breq2
⊢
x
=
B
→
B
≈
x
↔
B
≈
B
13
12
rspcev
⊢
B
∈
ω
∧
B
≈
B
→
∃
x
∈
ω
B
≈
x
14
10
11
13
syl2anc2
⊢
A
∈
ω
∧
B
=
A
→
∃
x
∈
ω
B
≈
x
15
8
14
jaodan
⊢
A
∈
ω
∧
B
⊂
A
∨
B
=
A
→
∃
x
∈
ω
B
≈
x
16
1
15
sylan2b
⊢
A
∈
ω
∧
B
⊆
A
→
∃
x
∈
ω
B
≈
x
17
isfi
⊢
B
∈
Fin
↔
∃
x
∈
ω
B
≈
x
18
16
17
sylibr
⊢
A
∈
ω
∧
B
⊆
A
→
B
∈
Fin