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 e. Fin /\ B C_ A ) -> B e. Fin )

Proof

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