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 ⊢ A ∈ Fin ∧ B ⊆ A → B ∈ Fin

Proof

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