This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )

Proof

Step Hyp Ref Expression
1 sspss ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) )
2 pssnn ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝐵 ≈ 𝑥 )
3 elnn ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ ω ) → 𝑥 ∈ ω )
4 3 expcom ⊢ ( 𝐴 ∈ ω → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ω ) )
5 4 anim1d ⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ≈ 𝑥 ) → ( 𝑥 ∈ ω ∧ 𝐵 ≈ 𝑥 ) ) )
6 5 reximdv2 ⊢ ( 𝐴 ∈ ω → ( ∃ 𝑥 ∈ 𝐴 𝐵 ≈ 𝑥 → ∃ 𝑥 ∈ ω 𝐵 ≈ 𝑥 ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ( ∃ 𝑥 ∈ 𝐴 𝐵 ≈ 𝑥 → ∃ 𝑥 ∈ ω 𝐵 ≈ 𝑥 ) )
8 2 7 mpd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → ∃ 𝑥 ∈ ω 𝐵 ≈ 𝑥 )
9 isfi ⊢ ( 𝐵 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐵 ≈ 𝑥 )
10 8 9 sylibr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊊ 𝐴 ) → 𝐵 ∈ Fin )
11 eleq1 ⊢ ( 𝐵 = 𝐴 → ( 𝐵 ∈ ω ↔ 𝐴 ∈ ω ) )
12 11 biimparc ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 = 𝐴 ) → 𝐵 ∈ ω )
13 nnfi ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ Fin )
14 12 13 syl ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 = 𝐴 ) → 𝐵 ∈ Fin )
15 10 14 jaodan ⊢ ( ( 𝐴 ∈ ω ∧ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ) → 𝐵 ∈ Fin )
16 1 15 sylan2b ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )