Metamath Proof Explorer

Theorem ssfi

Description: A subset of a finite set is finite. Corollary 6G of Enderton p. 138. (Contributed by NM, 24-Jun-1998)

Ref Expression
Assertion ssfi ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )

Proof

Step Hyp Ref Expression
1 isfi ⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 )
2 bren ⊢ ( 𝐴 ≈ 𝑥 ↔ ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝑥 )
3 f1ofo ⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → 𝑧 : 𝐴 –onto→ 𝑥 )
4 imassrn ⊢ ( 𝑧 “ 𝐵 ) ⊆ ran 𝑧
5 forn ⊢ ( 𝑧 : 𝐴 –onto→ 𝑥 → ran 𝑧 = 𝑥 )
6 4 5 sseqtrid ⊢ ( 𝑧 : 𝐴 –onto→ 𝑥 → ( 𝑧 “ 𝐵 ) ⊆ 𝑥 )
7 3 6 syl ⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → ( 𝑧 “ 𝐵 ) ⊆ 𝑥 )
8 ssnnfi ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 “ 𝐵 ) ⊆ 𝑥 ) → ( 𝑧 “ 𝐵 ) ∈ Fin )
9 isfi ⊢ ( ( 𝑧 “ 𝐵 ) ∈ Fin ↔ ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
10 8 9 sylib ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 “ 𝐵 ) ⊆ 𝑥 ) → ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
11 7 10 sylan2 ⊢ ( ( 𝑥 ∈ ω ∧ 𝑧 : 𝐴 –1-1-onto→ 𝑥 ) → ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
12 11 adantrr ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ) → ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 )
13 f1of1 ⊢ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → 𝑧 : 𝐴 –1-1→ 𝑥 )
14 f1ores ⊢ ( ( 𝑧 : 𝐴 –1-1→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
15 13 14 sylan ⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
16 vex ⊢ 𝑧 ∈ V
17 16 resex ⊢ ( 𝑧 ↾ 𝐵 ) ∈ V
18 f1oeq1 ⊢ ( 𝑥 = ( 𝑧 ↾ 𝐵 ) → ( 𝑥 : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) ↔ ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) ) )
19 17 18 spcev ⊢ ( ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) → ∃ 𝑥 𝑥 : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
20 bren ⊢ ( 𝐵 ≈ ( 𝑧 “ 𝐵 ) ↔ ∃ 𝑥 𝑥 : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) )
21 19 20 sylibr ⊢ ( ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) → 𝐵 ≈ ( 𝑧 “ 𝐵 ) )
22 entr ⊢ ( ( 𝐵 ≈ ( 𝑧 “ 𝐵 ) ∧ ( 𝑧 “ 𝐵 ) ≈ 𝑦 ) → 𝐵 ≈ 𝑦 )
23 21 22 sylan ⊢ ( ( ( 𝑧 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝑧 “ 𝐵 ) ∧ ( 𝑧 “ 𝐵 ) ≈ 𝑦 ) → 𝐵 ≈ 𝑦 )
24 15 23 sylan ⊢ ( ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ∧ ( 𝑧 “ 𝐵 ) ≈ 𝑦 ) → 𝐵 ≈ 𝑦 )
25 24 ex ⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑧 “ 𝐵 ) ≈ 𝑦 → 𝐵 ≈ 𝑦 ) )
26 25 reximdv ⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 → ∃ 𝑦 ∈ ω 𝐵 ≈ 𝑦 ) )
27 isfi ⊢ ( 𝐵 ∈ Fin ↔ ∃ 𝑦 ∈ ω 𝐵 ≈ 𝑦 )
28 26 27 syl6ibr ⊢ ( ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) → ( ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 → 𝐵 ∈ Fin ) )
29 28 adantl ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ) → ( ∃ 𝑦 ∈ ω ( 𝑧 “ 𝐵 ) ≈ 𝑦 → 𝐵 ∈ Fin ) )
30 12 29 mpd ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 ∧ 𝐵 ⊆ 𝐴 ) ) → 𝐵 ∈ Fin )
31 30 exp32 ⊢ ( 𝑥 ∈ ω → ( 𝑧 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
32 31 exlimdv ⊢ ( 𝑥 ∈ ω → ( ∃ 𝑧 𝑧 : 𝐴 –1-1-onto→ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
33 2 32 syl5bi ⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
34 33 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) )
35 1 34 sylbi ⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) )
36 35 imp ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )