Metamath Proof Explorer

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 enrefg ⊢ 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