Metamath Proof Explorer

Theorem ssfi

Description: A subset of a finite set is finite. Corollary 6G of Enderton p. 138. For a shorter proof using ax-pow , see ssfiALT . (Contributed by NM, 24-Jun-1998) Avoid ax-pow . (Revised by BTernaryTau, 12-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 ssexg ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐵 ∈ V )
2 1 ancoms ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V )
3 sseq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
4 eleq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ Fin ↔ 𝐵 ∈ Fin ) )
5 3 4 imbi12d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin ) ↔ ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
6 5 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ Fin → ( 𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin ) ) ↔ ( 𝐴 ∈ Fin → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) ) )
7 sseq2 ⊢ ( 𝑥 = ∅ → ( 𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ∅ ) )
8 7 imbi1d ⊢ ( 𝑥 = ∅ → ( ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ( 𝑏 ⊆ ∅ → 𝑏 ∈ Fin ) ) )
9 8 albidv ⊢ ( 𝑥 = ∅ → ( ∀ 𝑏 ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ∀ 𝑏 ( 𝑏 ⊆ ∅ → 𝑏 ∈ Fin ) ) )
10 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝑦 ) )
11 10 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) ) )
12 11 albidv ⊢ ( 𝑥 = 𝑦 → ( ∀ 𝑏 ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ∀ 𝑏 ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) ) )
13 sseq2 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) )
14 13 imbi1d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → 𝑏 ∈ Fin ) ) )
15 14 albidv ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ∀ 𝑏 ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ∀ 𝑏 ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → 𝑏 ∈ Fin ) ) )
16 sseq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑏 ⊆ 𝑥 ↔ 𝑏 ⊆ 𝐴 ) )
17 16 imbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ( 𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin ) ) )
18 17 albidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑏 ( 𝑏 ⊆ 𝑥 → 𝑏 ∈ Fin ) ↔ ∀ 𝑏 ( 𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin ) ) )
19 ss0 ⊢ ( 𝑏 ⊆ ∅ → 𝑏 = ∅ )
20 0fin ⊢ ∅ ∈ Fin
21 19 20 eqeltrdi ⊢ ( 𝑏 ⊆ ∅ → 𝑏 ∈ Fin )
22 21 ax-gen ⊢ ∀ 𝑏 ( 𝑏 ⊆ ∅ → 𝑏 ∈ Fin )
23 sseq1 ⊢ ( 𝑏 = 𝑐 → ( 𝑏 ⊆ 𝑦 ↔ 𝑐 ⊆ 𝑦 ) )
24 eleq1w ⊢ ( 𝑏 = 𝑐 → ( 𝑏 ∈ Fin ↔ 𝑐 ∈ Fin ) )
25 23 24 imbi12d ⊢ ( 𝑏 = 𝑐 → ( ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) ↔ ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ) )
26 25 cbvalvw ⊢ ( ∀ 𝑏 ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) ↔ ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) )
27 simp1 ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) )
28 snssi ⊢ ( 𝑧 ∈ 𝑏 → { 𝑧 } ⊆ 𝑏 )
29 undif ⊢ ( { 𝑧 } ⊆ 𝑏 ↔ ( { 𝑧 } ∪ ( 𝑏 ∖ { 𝑧 } ) ) = 𝑏 )
30 28 29 sylib ⊢ ( 𝑧 ∈ 𝑏 → ( { 𝑧 } ∪ ( 𝑏 ∖ { 𝑧 } ) ) = 𝑏 )
31 uncom ⊢ ( { 𝑧 } ∪ ( 𝑏 ∖ { 𝑧 } ) ) = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } )
32 30 31 eqtr3di ⊢ ( 𝑧 ∈ 𝑏 → 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) )
33 uncom ⊢ ( 𝑦 ∪ { 𝑧 } ) = ( { 𝑧 } ∪ 𝑦 )
34 33 sseq2i ⊢ ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ↔ 𝑏 ⊆ ( { 𝑧 } ∪ 𝑦 ) )
35 ssundif ⊢ ( 𝑏 ⊆ ( { 𝑧 } ∪ 𝑦 ) ↔ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 )
36 34 35 sylbb ⊢ ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 )
37 32 36 anim12ci ⊢ ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → ( ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
38 37 3adant1 ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → ( ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
39 3anass ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) ↔ ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ ( ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) ) )
40 27 38 39 sylanbrc ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) )
41 vex ⊢ 𝑏 ∈ V
42 41 difexi ⊢ ( 𝑏 ∖ { 𝑧 } ) ∈ V
43 sseq1 ⊢ ( 𝑐 = ( 𝑏 ∖ { 𝑧 } ) → ( 𝑐 ⊆ 𝑦 ↔ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ) )
44 eleq1 ⊢ ( 𝑐 = ( 𝑏 ∖ { 𝑧 } ) → ( 𝑐 ∈ Fin ↔ ( 𝑏 ∖ { 𝑧 } ) ∈ Fin ) )
45 43 44 imbi12d ⊢ ( 𝑐 = ( 𝑏 ∖ { 𝑧 } ) → ( ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ↔ ( ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 → ( 𝑏 ∖ { 𝑧 } ) ∈ Fin ) ) )
46 42 45 spcv ⊢ ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) → ( ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 → ( 𝑏 ∖ { 𝑧 } ) ∈ Fin ) )
47 46 imp ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ) → ( 𝑏 ∖ { 𝑧 } ) ∈ Fin )
48 snfi ⊢ { 𝑧 } ∈ Fin
49 unfi ⊢ ( ( ( 𝑏 ∖ { 𝑧 } ) ∈ Fin ∧ { 𝑧 } ∈ Fin ) → ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ∈ Fin )
50 47 48 49 sylancl ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ) → ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ∈ Fin )
51 eleq1 ⊢ ( 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) → ( 𝑏 ∈ Fin ↔ ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ∈ Fin ) )
52 51 biimparc ⊢ ( ( ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ∈ Fin ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin )
53 50 52 stoic3 ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ ( 𝑏 ∖ { 𝑧 } ) ⊆ 𝑦 ∧ 𝑏 = ( ( 𝑏 ∖ { 𝑧 } ) ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin )
54 40 53 syl ⊢ ( ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) ∧ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin )
55 54 3expib ⊢ ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) → ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) )
56 55 alrimiv ⊢ ( ∀ 𝑐 ( 𝑐 ⊆ 𝑦 → 𝑐 ∈ Fin ) → ∀ 𝑏 ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) )
57 26 56 sylbi ⊢ ( ∀ 𝑏 ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) → ∀ 𝑏 ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) )
58 disjsn ⊢ ( ( 𝑏 ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ 𝑏 )
59 disjssun ⊢ ( ( 𝑏 ∩ { 𝑧 } ) = ∅ → ( 𝑏 ⊆ ( { 𝑧 } ∪ 𝑦 ) ↔ 𝑏 ⊆ 𝑦 ) )
60 58 59 sylbir ⊢ ( ¬ 𝑧 ∈ 𝑏 → ( 𝑏 ⊆ ( { 𝑧 } ∪ 𝑦 ) ↔ 𝑏 ⊆ 𝑦 ) )
61 60 biimpa ⊢ ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( { 𝑧 } ∪ 𝑦 ) ) → 𝑏 ⊆ 𝑦 )
62 34 61 sylan2b ⊢ ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ⊆ 𝑦 )
63 62 imim1i ⊢ ( ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) → ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) )
64 63 alimi ⊢ ( ∀ 𝑏 ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) → ∀ 𝑏 ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) )
65 exmid ⊢ ( 𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏 )
66 65 jctl ⊢ ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏 ) ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) )
67 andir ⊢ ( ( ( 𝑧 ∈ 𝑏 ∨ ¬ 𝑧 ∈ 𝑏 ) ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ↔ ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ∨ ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ) )
68 66 67 sylib ⊢ ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ∨ ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ) )
69 pm3.44 ⊢ ( ( ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) ∧ ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) ) → ( ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ∨ ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) ) → 𝑏 ∈ Fin ) )
70 68 69 syl5 ⊢ ( ( ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) ∧ ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) ) → ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → 𝑏 ∈ Fin ) )
71 70 alanimi ⊢ ( ( ∀ 𝑏 ( ( 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) ∧ ∀ 𝑏 ( ( ¬ 𝑧 ∈ 𝑏 ∧ 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) ) → 𝑏 ∈ Fin ) ) → ∀ 𝑏 ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → 𝑏 ∈ Fin ) )
72 57 64 71 syl2anc ⊢ ( ∀ 𝑏 ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) → ∀ 𝑏 ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → 𝑏 ∈ Fin ) )
73 72 a1i ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑏 ( 𝑏 ⊆ 𝑦 → 𝑏 ∈ Fin ) → ∀ 𝑏 ( 𝑏 ⊆ ( 𝑦 ∪ { 𝑧 } ) → 𝑏 ∈ Fin ) ) )
74 9 12 15 18 22 73 findcard2 ⊢ ( 𝐴 ∈ Fin → ∀ 𝑏 ( 𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin ) )
75 74 19.21bi ⊢ ( 𝐴 ∈ Fin → ( 𝑏 ⊆ 𝐴 → 𝑏 ∈ Fin ) )
76 6 75 vtoclg ⊢ ( 𝐵 ∈ V → ( 𝐴 ∈ Fin → ( 𝐵 ⊆ 𝐴 → 𝐵 ∈ Fin ) ) )
77 76 impd ⊢ ( 𝐵 ∈ V → ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin ) )
78 2 77 mpcom ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )