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=∅→∀bb⊆x→b∈Fin↔∀bb⊆∅→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→∀bb⊆x→b∈Fin↔∀bb⊆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→∀bb⊆x→b∈Fin↔∀bb⊆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→∀bb⊆x→b∈Fin↔∀bb⊆A→b∈Fin
19 ss0 ⊢b⊆∅→b=∅
20 0fin ⊢∅∈Fin
21 19 20 eqeltrdi ⊢b⊆∅→b∈Fin
22 21 ax-gen ⊢∀bb⊆∅→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 ⊢∀bb⊆y→b∈Fin↔∀cc⊆y→c∈Fin
27 simp1 ⊢∀cc⊆y→c∈Fin∧z∈b∧b⊆y∪z→∀cc⊆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 ⊢∀cc⊆y→c∈Fin∧z∈b∧b⊆y∪z→b∖z⊆y∧b=b∖z∪z
39 3anass ⊢∀cc⊆y→c∈Fin∧b∖z⊆y∧b=b∖z∪z↔∀cc⊆y→c∈Fin∧b∖z⊆y∧b=b∖z∪z
40 27 38 39 sylanbrc ⊢∀cc⊆y→c∈Fin∧z∈b∧b⊆y∪z→∀cc⊆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 ⊢∀cc⊆y→c∈Fin→b∖z⊆y→b∖z∈Fin
47 46 imp ⊢∀cc⊆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 ⊢∀cc⊆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 ⊢∀cc⊆y→c∈Fin∧b∖z⊆y∧b=b∖z∪z→b∈Fin
54 40 53 syl ⊢∀cc⊆y→c∈Fin∧z∈b∧b⊆y∪z→b∈Fin
55 54 3expib ⊢∀cc⊆y→c∈Fin→z∈b∧b⊆y∪z→b∈Fin
56 55 alrimiv ⊢∀cc⊆y→c∈Fin→∀bz∈b∧b⊆y∪z→b∈Fin
57 26 56 sylbi ⊢∀bb⊆y→b∈Fin→∀bz∈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 ⊢∀bb⊆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 ⊢∀bz∈b∧b⊆y∪z→b∈Fin∧∀b¬z∈b∧b⊆y∪z→b∈Fin→∀bb⊆y∪z→b∈Fin
72 57 64 71 syl2anc ⊢∀bb⊆y→b∈Fin→∀bb⊆y∪z→b∈Fin
73 72 a1i ⊢y∈Fin→∀bb⊆y→b∈Fin→∀bb⊆y∪z→b∈Fin
74 9 12 15 18 22 73 findcard2 ⊢A∈Fin→∀bb⊆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