NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ssfin Unicode version

Theorem ssfin 4470
Description: A subset of a finite set is itself finite. Theorem X.1.21 of [Rosser] p. 527. (Contributed by SF, 19-Jan-2015.)
Assertion
Ref Expression
ssfin Fin Fin

Proof of Theorem ssfin
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3292 . . . . 5
2 eleq1 2413 . . . . 5 Fin Fin
31, 2imbi12d 311 . . . 4 Fin Fin
43imbi2d 307 . . 3 Fin Fin Fin Fin
5 sseq2 3293 . . . . 5
65imbi1d 308 . . . 4 Fin Fin
7 elfin 4420 . . . . 5 Fin Nn
8 vex 2862 . . . . . . . . . . . . 13
98elcompl 3225 . . . . . . . . . . . 12 Sk 1 Sk kFin k k1c Sk 1 Sk kFin k k1c
10 alcom 1737 . . . . . . . . . . . . 13 Fin Fin
11 impexp 433 . . . . . . . . . . . . . . . 16 Fin Fin
1211albii 1566 . . . . . . . . . . . . . . 15 Fin Fin
13 19.21v 1890 . . . . . . . . . . . . . . 15 Fin Fin
1412, 13bitri 240 . . . . . . . . . . . . . 14 Fin Fin
1514albii 1566 . . . . . . . . . . . . 13 Fin Fin
168elimak 4259 . . . . . . . . . . . . . . 15 Sk 1 Sk kFin k k1c 1c Sk 1 Sk kFin k
17 df-rex 2620 . . . . . . . . . . . . . . . 16 1c Sk 1 Sk kFin k 1c Sk 1 Sk kFin k
18 el1c 4139 . . . . . . . . . . . . . . . . . . . 20 1c
1918anbi1i 676 . . . . . . . . . . . . . . . . . . 19 1c Sk 1 Sk kFin k Sk 1 Sk kFin k
20 19.41v 1901 . . . . . . . . . . . . . . . . . . 19 Sk 1 Sk kFin k Sk 1 Sk kFin k
2119, 20bitr4i 243 . . . . . . . . . . . . . . . . . 18 1c Sk 1 Sk kFin k Sk 1 Sk kFin k
2221exbii 1582 . . . . . . . . . . . . . . . . 17 1c Sk 1 Sk kFin k Sk 1 Sk kFin k
23 excom 1741 . . . . . . . . . . . . . . . . 17 Sk 1 Sk kFin k Sk 1 Sk kFin k
2422, 23bitr4i 243 . . . . . . . . . . . . . . . 16 1c Sk 1 Sk kFin k Sk 1 Sk kFin k
25 snex 4111 . . . . . . . . . . . . . . . . . . 19
26 opkeq1 4059 . . . . . . . . . . . . . . . . . . . 20
2726eleq1d 2419 . . . . . . . . . . . . . . . . . . 19 Sk 1 Sk kFin k Sk 1 Sk kFin k
2825, 27ceqsexv 2894 . . . . . . . . . . . . . . . . . 18 Sk 1 Sk kFin k Sk 1 Sk kFin k
29 elin 3219 . . . . . . . . . . . . . . . . . 18 Sk 1 Sk kFin k Sk 1 Sk kFin k
30 vex 2862 . . . . . . . . . . . . . . . . . . . 20
3130, 8elssetk 4270 . . . . . . . . . . . . . . . . . . 19 Sk
3225, 8opkelxpk 4248 . . . . . . . . . . . . . . . . . . . . 21 1 Sk kFin k 1 Sk kFin
338, 32mpbiran2 885 . . . . . . . . . . . . . . . . . . . 20 1 Sk kFin k 1 Sk kFin
34 snelpw1 4146 . . . . . . . . . . . . . . . . . . . 20 1 Sk kFin Sk kFin
3530elimak 4259 . . . . . . . . . . . . . . . . . . . . 21 Sk kFin Fin Sk
36 df-rex 2620 . . . . . . . . . . . . . . . . . . . . . 22 Fin Sk Fin Sk
37 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . 24 Fin Sk Sk Fin
38 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . 26
39 opkelssetkg 4268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Sk
4038, 30, 39mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . 25 Sk
4138elcompl 3225 . . . . . . . . . . . . . . . . . . . . . . . . 25 Fin Fin
4240, 41anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 Sk Fin Fin
4337, 42bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 Fin Sk Fin
4443exbii 1582 . . . . . . . . . . . . . . . . . . . . . 22 Fin Sk Fin
4536, 44bitri 240 . . . . . . . . . . . . . . . . . . . . 21 Fin Sk Fin
46 exanali 1585 . . . . . . . . . . . . . . . . . . . . 21 Fin Fin
4735, 45, 463bitri 262 . . . . . . . . . . . . . . . . . . . 20 Sk kFin Fin
4833, 34, 473bitri 262 . . . . . . . . . . . . . . . . . . 19 1 Sk kFin k Fin
4931, 48anbi12i 678 . . . . . . . . . . . . . . . . . 18 Sk 1 Sk kFin k Fin
5028, 29, 493bitri 262 . . . . . . . . . . . . . . . . 17 Sk 1 Sk kFin k Fin
5150exbii 1582 . . . . . . . . . . . . . . . 16 Sk 1 Sk kFin k Fin
5217, 24, 513bitri 262 . . . . . . . . . . . . . . 15 1c Sk 1 Sk kFin k Fin
53 exanali 1585 . . . . . . . . . . . . . . 15 Fin Fin
5416, 52, 533bitri 262 . . . . . . . . . . . . . 14 Sk 1 Sk kFin k k1c Fin
5554con2bii 322 . . . . . . . . . . . . 13 Fin Sk 1 Sk kFin k k1c
5610, 15, 553bitri 262 . . . . . . . . . . . 12 Fin Sk 1 Sk kFin k k1c
579, 56bitr4i 243 . . . . . . . . . . 11 Sk 1 Sk kFin k k1c Fin
5857abbi2i 2464 . . . . . . . . . 10 Sk 1 Sk kFin k k1c Fin
59 ssetkex 4294 . . . . . . . . . . . . 13 Sk
60 finex 4397 . . . . . . . . . . . . . . . . 17 Fin
6160complex 4104 . . . . . . . . . . . . . . . 16 Fin
6259, 61imakex 4300 . . . . . . . . . . . . . . 15 Sk kFin
6362pw1ex 4303 . . . . . . . . . . . . . 14 1 Sk kFin
64 vvex 4109 . . . . . . . . . . . . . 14
6563, 64xpkex 4289 . . . . . . . . . . . . 13 1 Sk kFin k
6659, 65inex 4105 . . . . . . . . . . . 12 Sk 1 Sk kFin k
67 1cex 4142 . . . . . . . . . . . 12 1c
6866, 67imakex 4300 . . . . . . . . . . 11 Sk 1 Sk kFin k k1c
6968complex 4104 . . . . . . . . . 10 Sk 1 Sk kFin k k1c
7058, 69eqeltrri 2424 . . . . . . . . 9 Fin
71 eleq2 2414 . . . . . . . . . . . . 13 0c 0c
72 df-0c 4377 . . . . . . . . . . . . . . 15 0c
7372eleq2i 2417 . . . . . . . . . . . . . 14 0c
7430elsnc 3756 . . . . . . . . . . . . . 14
7573, 74bitri 240 . . . . . . . . . . . . 13 0c
7671, 75syl6bb 252 . . . . . . . . . . . 12 0c
7776anbi1d 685 . . . . . . . . . . 11 0c
7877imbi1d 308 . . . . . . . . . 10 0c Fin Fin
79782albidv 1627 . . . . . . . . 9 0c Fin Fin
80 elequ2 1715 . . . . . . . . . . . . 13
8180anbi1d 685 . . . . . . . . . . . 12
8281imbi1d 308 . . . . . . . . . . 11 Fin Fin
83822albidv 1627 . . . . . . . . . 10 Fin Fin
84 eleq1 2413 . . . . . . . . . . . . . 14
8584adantl 452 . . . . . . . . . . . . 13
86 sseq12 3294 . . . . . . . . . . . . 13
8785, 86anbi12d 691 . . . . . . . . . . . 12
88 eleq1 2413 . . . . . . . . . . . . 13 Fin Fin
8988adantr 451 . . . . . . . . . . . 12 Fin Fin
9087, 89imbi12d 311 . . . . . . . . . . 11 Fin Fin
9190cbval2v 2006 . . . . . . . . . 10 Fin Fin
9283, 91syl6bb 252 . . . . . . . . 9 Fin Fin
93 eleq2 2414 . . . . . . . . . . . 12 1c 1c
9493anbi1d 685 . . . . . . . . . . 11 1c 1c
9594imbi1d 308 . . . . . . . . . 10 1c Fin 1c Fin
96952albidv 1627 . . . . . . . . 9 1c Fin 1c Fin
97 elequ2 1715 . . . . . . . . . . . 12
9897anbi1d 685 . . . . . . . . . . 11
9998imbi1d 308 . . . . . . . . . 10 Fin Fin
100992albidv 1627 . . . . . . . . 9 Fin Fin
101 sseq2 3293 . . . . . . . . . . . . 13
102101biimpa 470 . . . . . . . . . . . 12
103 ss0b 3580 . . . . . . . . . . . 12
104102, 103sylib 188 . . . . . . . . . . 11
105 0fin 4423 . . . . . . . . . . 11 Fin
106104, 105syl6eqel 2441 . . . . . . . . . 10 Fin
107106gen2 1547 . . . . . . . . 9 Fin
108 sspss 3368 . . . . . . . . . . . . . . 15
109 dfpss4 3888 . . . . . . . . . . . . . . . 16
110109orbi1i 506 . . . . . . . . . . . . . . 15
111108, 110bitri 240 . . . . . . . . . . . . . 14
112 simp1 955 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn 1c Nn
113 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
114113snid 3760 . . . . . . . . . . . . . . . . . . . . . . . . . 26
115 eldif 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
116115simprbi 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26
117114, 116mt2 170 . . . . . . . . . . . . . . . . . . . . . . . . 25
118117a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn 1c
119 undif1 3625 . . . . . . . . . . . . . . . . . . . . . . . . . 26
120 snssi 3852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121 ssequn2 3436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
122120, 121sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
123122adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1241233ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn 1c
125119, 124syl5eq 2397 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nn 1c
126 simp3r 984 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nn 1c 1c
127125, 126eqeltrd 2427 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn 1c 1c
128 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . 26
12930, 128difex 4107 . . . . . . . . . . . . . . . . . . . . . . . . 25
130129, 113nnsucelr 4428 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn 1c
131112, 118, 127, 130syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . 23 Nn 1c
132 inass 3465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
133 df-dif 3215 . . . . . . . . . . . . . . . . . . . . . . . . . 26
134 df-dif 3215 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
135134ineq2i 3454 . . . . . . . . . . . . . . . . . . . . . . . . . 26
136132, 133, 1353eqtr4ri 2384 . . . . . . . . . . . . . . . . . . . . . . . . 25
137 df-ss 3259 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
138137biimpi 186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
139138adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1c
1401393ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Nn 1c
141140difeq1d 3384 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn 1c
142 difsn 3845 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
143142adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
1441433ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Nn 1c
145141, 144eqtrd 2385 . . . . . . . . . . . . . . . . . . . . . . . . 25 Nn 1c
146136, 145syl5eq 2397 . . . . . . . . . . . . . . . . . . . . . . . 24 Nn 1c
147 df-ss 3259 . . . . . . . . . . . . . . . . . . . . . . . 24
148146, 147sylibr 203 . . . . . . . . . . . . . . . . . . . . . . 23 Nn 1c
149131, 148jca 518 . . . . . . . . . . . . . . . . . . . . . 22 Nn 1c
1501493adant1r 1175 . . . . . . . . . . . . . . . . . . . . 21 Nn Fin 1c
151 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
152151adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
153 sseq12 3294 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
154152, 153anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26
155 eleq1 2413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Fin Fin
156155adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Fin Fin
157154, 156imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . 25 Fin Fin
158157spc2gv 2942 . . . . . . . . . . . . . . . . . . . . . . . 24 Fin Fin
15938, 129, 158mp2an 653 . . . . . . . . . . . . . . . . . . . . . . 23 Fin Fin
160159adantl 452 . . . . . . . . . . . . . . . . . . . . . 22 Nn Fin Fin
1611603ad2ant1 976 . . . . . . . . . . . . . . . . . . . . 21 Nn Fin 1c Fin
162150, 161mpd 14 . . . . . . . . . . . . . . . . . . . 20 Nn Fin 1c Fin
1631623exp 1150 . . . . . . . . . . . . . . . . . . 19 Nn Fin 1c Fin
164163exp5c 599 . . . . . . . . . . . . . . . . . 18 Nn Fin 1c Fin
165164rexlimdv 2737 . . . . . . . . . . . . . . . . 17 Nn Fin 1c Fin
166165com23 72 . . . . . . . . . . . . . . . 16 Nn Fin 1c Fin
167166imp3a 420 . . . . . . . . . . . . . . 15 Nn Fin 1c Fin
168 peano2 4403 . . . . . . . . . . . . . . . . . 18 Nn 1c Nn
169 eleq2 2414 . . . . . . . . . . . . . . . . . . . . 21 1c 1c
170169rspcev 2955 . . . . . . . . . . . . . . . . . . . 20 1c Nn 1c Nn
171 elfin 4420 . . . . . . . . . . . . . . . . . . . 20 Fin Nn
172170, 171sylibr 203 . . . . . . . . . . . . . . . . . . 19 1c Nn 1c Fin
173172ex 423 . . . . . . . . . . . . . . . . . 18 1c Nn 1c Fin
174168, 173syl 15 . . . . . . . . . . . . . . . . 17 Nn 1c Fin
175 eleq1 2413 . . . . . . . . . . . . . . . . . 18 Fin Fin
176175biimprd 214 . . . . . . . . . . . . . . . . 17 Fin Fin
177174, 176syl9 66 . . . . . . . . . . . . . . . 16 Nn 1c Fin
178177adantr 451 . . . . . . . . . . . . . . 15 Nn Fin 1c Fin
179167, 178jaod 369 . . . . . . . . . . . . . 14 Nn Fin 1c Fin
180111, 179syl5bi 208 . . . . . . . . . . . . 13 Nn Fin 1c Fin
181180com23 72 . . . . . . . . . . . 12 Nn Fin 1c Fin
182181imp3a 420 . . . . . . . . . . 11 Nn Fin 1c Fin
183182alrimivv 1632 . . . . . . . . . 10 Nn Fin 1c Fin
184183ex 423 . . . . . . . . 9 Nn Fin 1c Fin
18570, 79, 92, 96, 100, 107, 184finds 4411 . . . . . . . 8 Nn Fin
18618519.21bbi 1865 . . . . . . 7 Nn Fin
187186exp3a 425 . . . . . 6 Nn Fin
188187rexlimiv 2732 . . . . 5 Nn Fin
1897, 188sylbi 187 . . . 4 Fin Fin
1906, 189vtoclga 2920 . . 3 Fin Fin
1914, 190vtoclg 2914 . 2 Fin Fin
1921913imp 1145 1 Fin Fin
Colors of variables: wff setvar class
Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934  wal 1540  wex 1541   wceq 1642   wcel 1710  cab 2339  wrex 2615  cvv 2859   ∼ ccompl 3205   cdif 3206   cun 3207   cin 3208   wss 3257   wpss 3258  c0 3550  csn 3737  copk 4057  1cc1c 4134  1 cpw1 4135   k cxpk 4174  kcimak 4179   Sk cssetk 4183   Nn cnnc 4373  0cc0c 4374   cplc 4375   Fin cfin 4376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380
This theorem is referenced by:  vfinnc  4471  sfinltfin  4535
  Copyright terms: Public domain W3C validator