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		enrefnn	⊢ ( 𝐵 ∈ ω → 𝐵 ≈ 𝐵 )
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 )