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 )