Metamath Proof Explorer


Theorem ssnnfi

Description: A subset of a natural number is finite. (Contributed by NM, 24-Jun-1998)

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 eleq1 ( 𝐵 = 𝐴 → ( 𝐵 ∈ ω ↔ 𝐴 ∈ ω ) )
10 9 biimparc ( ( 𝐴 ∈ ω ∧ 𝐵 = 𝐴 ) → 𝐵 ∈ ω )
11 enrefg ( 𝐵 ∈ ω → 𝐵𝐵 )
12 breq2 ( 𝑥 = 𝐵 → ( 𝐵𝑥𝐵𝐵 ) )
13 12 rspcev ( ( 𝐵 ∈ ω ∧ 𝐵𝐵 ) → ∃ 𝑥 ∈ ω 𝐵𝑥 )
14 10 11 13 syl2anc2 ( ( 𝐴 ∈ ω ∧ 𝐵 = 𝐴 ) → ∃ 𝑥 ∈ ω 𝐵𝑥 )
15 8 14 jaodan ( ( 𝐴 ∈ ω ∧ ( 𝐵𝐴𝐵 = 𝐴 ) ) → ∃ 𝑥 ∈ ω 𝐵𝑥 )
16 1 15 sylan2b ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → ∃ 𝑥 ∈ ω 𝐵𝑥 )
17 isfi ( 𝐵 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐵𝑥 )
18 16 17 sylibr ( ( 𝐴 ∈ ω ∧ 𝐵𝐴 ) → 𝐵 ∈ Fin )