MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  findcard2 Unicode version

Theorem findcard2 7460
Description: Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 8-Jul-2010.)
Hypotheses
Ref Expression
findcard2.1
findcard2.2
findcard2.3
findcard2.4
findcard2.5
findcard2.6
Assertion
Ref Expression
findcard2
Distinct variable groups:   , , ,   ,   ,   ,   ,   , ,
Allowed substitution hints:   ( )   ( , )   ( , )   ( , )   ( , )

Proof of Theorem findcard2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2.4 . 2
2 isfi 7243 . . 3
3 breq2 4306 . . . . . . . 8
43imbi1d 310 . . . . . . 7
54albidv 1645 . . . . . 6
6 breq2 4306 . . . . . . . 8
76imbi1d 310 . . . . . . 7
87albidv 1645 . . . . . 6
9 breq2 4306 . . . . . . . 8
109imbi1d 310 . . . . . . 7
1110albidv 1645 . . . . . 6
12 en0 7282 . . . . . . . 8
13 findcard2.5 . . . . . . . . 9
14 findcard2.1 . . . . . . . . 9
1513, 14mpbiri 226 . . . . . . . 8
1612, 15sylbi 189 . . . . . . 7
1716ax-gen 1562 . . . . . 6
18 nsuceq0 4802 . . . . . . . . . . . 12
19 breq1 4305 . . . . . . . . . . . . . . . 16
2019anbi2d 686 . . . . . . . . . . . . . . 15
21 peano1 6460 . . . . . . . . . . . . . . . . . 18
22 peano2 6461 . . . . . . . . . . . . . . . . . 18
23 nneneq 7402 . . . . . . . . . . . . . . . . . 18
2421, 22, 23sylancr 646 . . . . . . . . . . . . . . . . 17
2524biimpa 472 . . . . . . . . . . . . . . . 16
2625eqcomd 2486 . . . . . . . . . . . . . . 15
2720, 26syl6bi 221 . . . . . . . . . . . . . 14
2827com12 30 . . . . . . . . . . . . 13
2928necon3d 2684 . . . . . . . . . . . 12
3018, 29mpi 17 . . . . . . . . . . 11
3130ex 425 . . . . . . . . . 10
32 n0 3669 . . . . . . . . . . . 12
33 dif1en 7453 . . . . . . . . . . . . . . 15
34333expia 1163 . . . . . . . . . . . . . 14
35 snssi 4027 . . . . . . . . . . . . . . . . . 18
36 uncom 3524 . . . . . . . . . . . . . . . . . . 19
37 undif 3781 . . . . . . . . . . . . . . . . . . . 20
3837biimpi 188 . . . . . . . . . . . . . . . . . . 19
3936, 38syl5eq 2525 . . . . . . . . . . . . . . . . . 18
40 vex 3009 . . . . . . . . . . . . . . . . . . . . 21
41 difexg 4450 . . . . . . . . . . . . . . . . . . . . 21
4240, 41ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
43 breq1 4305 . . . . . . . . . . . . . . . . . . . . . 22
4443anbi2d 686 . . . . . . . . . . . . . . . . . . . . 21
45 uneq1 3527 . . . . . . . . . . . . . . . . . . . . . . 23
46 dfsbcq 3214 . . . . . . . . . . . . . . . . . . . . . . 23
4745, 46syl 16 . . . . . . . . . . . . . . . . . . . . . 22
4847imbi2d 309 . . . . . . . . . . . . . . . . . . . . 21
4944, 48imbi12d 313 . . . . . . . . . . . . . . . . . . . 20
50 breq1 4305 . . . . . . . . . . . . . . . . . . . . . . . 24
51 findcard2.2 . . . . . . . . . . . . . . . . . . . . . . . 24
5250, 51imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . 23
5352spv 1964 . . . . . . . . . . . . . . . . . . . . . 22
54 rspe 2813 . . . . . . . . . . . . . . . . . . . . . . . 24
55 isfi 7243 . . . . . . . . . . . . . . . . . . . . . . . 24
5654, 55sylibr 205 . . . . . . . . . . . . . . . . . . . . . . 23
57 pm2.27 38 . . . . . . . . . . . . . . . . . . . . . . . 24
5857adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23
59 findcard2.6 . . . . . . . . . . . . . . . . . . . . . . 23
6056, 58, 59sylsyld 55 . . . . . . . . . . . . . . . . . . . . . 22
6153, 60syl5 31 . . . . . . . . . . . . . . . . . . . . 21
62 vex 3009 . . . . . . . . . . . . . . . . . . . . . . 23
63 snex 4540 . . . . . . . . . . . . . . . . . . . . . . 23
6462, 63unex 6344 . . . . . . . . . . . . . . . . . . . . . 22
65 findcard2.3 . . . . . . . . . . . . . . . . . . . . . 22
6664, 65sbcie 3246 . . . . . . . . . . . . . . . . . . . . 21
6761, 66syl6ibr 220 . . . . . . . . . . . . . . . . . . . 20
6842, 49, 67vtocl 3056 . . . . . . . . . . . . . . . . . . 19
69 dfsbcq 3214 . . . . . . . . . . . . . . . . . . . 20
7069imbi2d 309 . . . . . . . . . . . . . . . . . . 19
7168, 70syl5ib 212 . . . . . . . . . . . . . . . . . 18
7235, 39, 713syl 19 . . . . . . . . . . . . . . . . 17
7372exp3a 427 . . . . . . . . . . . . . . . 16
7473com12 30 . . . . . . . . . . . . . . 15
7574adantr 453 . . . . . . . . . . . . . 14
7634, 75mpdd 39 . . . . . . . . . . . . 13
7776exlimdv 1656 . . . . . . . . . . . 12
7832, 77syl5bi 210 . . . . . . . . . . 11
7978ex 425 . . . . . . . . . 10
8031, 79mpdd 39 . . . . . . . . 9
8180com23 75 . . . . . . . 8
8281alrimdv 1653 . . . . . . 7
83 nfv 1639 . . . . . . . 8
84 nfv 1639 . . . . . . . . 9
85 nfsbc1v 3231 . . . . . . . . 9
8684, 85nfim 1830 . . . . . . . 8
87 breq1 4305 . . . . . . . . 9
88 sbceq1a 3222 . . . . . . . . 9
8987, 88imbi12d 313 . . . . . . . 8
9083, 86, 89cbval 1981 . . . . . . 7
9182, 90syl6ibr 220 . . . . . 6
925, 8, 11, 17, 91finds1 6470 . . . . 5
939219.21bi 1773 . . . 4
9493rexlimiv 2870 . . 3
952, 94sylbi 189 . 2
961, 95vtoclga 3067 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  A.wal 1556  E.wex 1557  =wceq 1662  e.wcel 1724  =/=wne 2644  E.wrex 2752   cvv 3006  [.wsbc 3212  \cdif 3350  u.cun 3351  C_wss 3353   c0 3660  {csn 3894   class class class wbr 4302  succsuc 4724   com 6441   cen 7218   cfn 7221
This theorem is referenced by:  findcard2s  7461  frfi  7464  fnfi  7496  iunfi  7506  finsschain  7525  infdiffi  7724  fin1a2lem10  8403  wunfi  8710  rexfiuz  12621  drsdirfi  14886  fiuncmp  17970  finiunmbl  19942  mbfresfi  27109  heibor1lem  27381  modfsummod  29104  pclfinclN  32020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-4 1573  ax-5 1636  ax-6 1677  ax-7 1697  ax-8 1726  ax-9 1728  ax-10 1743  ax-11 1748  ax-12 1760  ax-13 1947  ax-ext 2462  ax-sep 4423  ax-nul 4431  ax-pow 4477  ax-pr 4538  ax-un 6338
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1337  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2309  df-mo 2310  df-clab 2468  df-cleq 2474  df-clel 2477  df-nfc 2606  df-ne 2646  df-ral 2756  df-rex 2757  df-rab 2760  df-v 3008  df-sbc 3213  df-dif 3356  df-un 3358  df-in 3360  df-ss 3367  df-pss 3369  df-nul 3661  df-if 3813  df-pw 3880  df-sn 3900  df-pr 3901  df-tp 3902  df-op 3903  df-uni 4102  df-br 4303  df-opab 4361  df-tr 4396  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4850  df-rel 4851  df-cnv 4852  df-co 4853  df-dm 4854  df-rn 4855  df-res 4856  df-ima 4857  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-om 6442  df-1o 6836  df-er 7017  df-en 7222  df-fin 7225
  Copyright terms: Public domain W3C validator