Metamath Proof Explorer

Theorem ssnnfi

Description: A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998) (Proof shortened by BTernaryTau, 23-Sep-2024)

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 isfi ⊢ B ∈ Fin ↔ ∃ x ∈ ω B ≈ x
10 8 9 sylibr ⊢ A ∈ ω ∧ B ⊂ A → B ∈ Fin
11 eleq1 ⊢ B = A → B ∈ ω ↔ A ∈ ω
12 11 biimparc ⊢ A ∈ ω ∧ B = A → B ∈ ω
13 nnfi ⊢ B ∈ ω → B ∈ Fin
14 12 13 syl ⊢ A ∈ ω ∧ B = A → B ∈ Fin
15 10 14 jaodan ⊢ A ∈ ω ∧ B ⊂ A ∨ B = A → B ∈ Fin
16 1 15 sylan2b ⊢ A ∈ ω ∧ B ⊆ A → B ∈ Fin