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

Theorem findcard2 7513
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 7295 . . 3
3 breq2 4322 . . . . . . . 8
43imbi1d 310 . . . . . . 7
54albidv 1653 . . . . . 6
6 breq2 4322 . . . . . . . 8
76imbi1d 310 . . . . . . 7
87albidv 1653 . . . . . 6
9 breq2 4322 . . . . . . . 8
109imbi1d 310 . . . . . . 7
1110albidv 1653 . . . . . 6
12 en0 7334 . . . . . . . 8
13 findcard2.5 . . . . . . . . 9
14 findcard2.1 . . . . . . . . 9
1513, 14mpbiri 226 . . . . . . . 8
1612, 15sylbi 189 . . . . . . 7
1716ax-gen 1570 . . . . . 6
18 nsuceq0 4820 . . . . . . . . . . . 12
19 breq1 4321 . . . . . . . . . . . . . . . 16
2019anbi2d 686 . . . . . . . . . . . . . . 15
21 peano1 6505 . . . . . . . . . . . . . . . . . 18
22 peano2 6506 . . . . . . . . . . . . . . . . . 18
23 nneneq 7455 . . . . . . . . . . . . . . . . . 18
2421, 22, 23sylancr 646 . . . . . . . . . . . . . . . . 17
2524biimpa 472 . . . . . . . . . . . . . . . 16
2625eqcomd 2494 . . . . . . . . . . . . . . 15
2720, 26syl6bi 221 . . . . . . . . . . . . . 14
2827com12 30 . . . . . . . . . . . . 13
2928necon3d 2692 . . . . . . . . . . . 12
3018, 29mpi 17 . . . . . . . . . . 11
3130ex 425 . . . . . . . . . 10
32 n0 3682 . . . . . . . . . . . 12
33 dif1en 7506 . . . . . . . . . . . . . . 15
34333expia 1163 . . . . . . . . . . . . . 14
35 snssi 4042 . . . . . . . . . . . . . . . . . 18
36 uncom 3537 . . . . . . . . . . . . . . . . . . 19
37 undif 3794 . . . . . . . . . . . . . . . . . . . 20
3837biimpi 188 . . . . . . . . . . . . . . . . . . 19
3936, 38syl5eq 2533 . . . . . . . . . . . . . . . . . 18
40 vex 3018 . . . . . . . . . . . . . . . . . . . . 21
41 difexg 4466 . . . . . . . . . . . . . . . . . . . . 21
4240, 41ax-mp 5 . . . . . . . . . . . . . . . . . . . 20
43 breq1 4321 . . . . . . . . . . . . . . . . . . . . . 22
4443anbi2d 686 . . . . . . . . . . . . . . . . . . . . 21
45 uneq1 3540 . . . . . . . . . . . . . . . . . . . . . . 23
46 dfsbcq 3226 . . . . . . . . . . . . . . . . . . . . . . 23
4745, 46syl 16 . . . . . . . . . . . . . . . . . . . . . 22
4847imbi2d 309 . . . . . . . . . . . . . . . . . . . . 21
4944, 48imbi12d 313 . . . . . . . . . . . . . . . . . . . 20
50 breq1 4321 . . . . . . . . . . . . . . . . . . . . . . . 24
51 findcard2.2 . . . . . . . . . . . . . . . . . . . . . . . 24
5250, 51imbi12d 313 . . . . . . . . . . . . . . . . . . . . . . 23
5352spv 1972 . . . . . . . . . . . . . . . . . . . . . 22
54 rspe 2821 . . . . . . . . . . . . . . . . . . . . . . . 24
55 isfi 7295 . . . . . . . . . . . . . . . . . . . . . . . 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 3018 . . . . . . . . . . . . . . . . . . . . . . 23
63 snex 4556 . . . . . . . . . . . . . . . . . . . . . . 23
6462, 63unex 6388 . . . . . . . . . . . . . . . . . . . . . 22
65 findcard2.3 . . . . . . . . . . . . . . . . . . . . . 22
6664, 65sbcie 3258 . . . . . . . . . . . . . . . . . . . . 21
6761, 66syl6ibr 220 . . . . . . . . . . . . . . . . . . . 20
6842, 49, 67vtocl 3065 . . . . . . . . . . . . . . . . . . 19
69 dfsbcq 3226 . . . . . . . . . . . . . . . . . . . 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 1664 . . . . . . . . . . . 12
7832, 77syl5bi 210 . . . . . . . . . . 11
7978ex 425 . . . . . . . . . 10
8031, 79mpdd 39 . . . . . . . . 9
8180com23 75 . . . . . . . 8
8281alrimdv 1661 . . . . . . 7
83 nfv 1647 . . . . . . . 8
84 nfv 1647 . . . . . . . . 9
85 nfsbc1v 3243 . . . . . . . . 9
8684, 85nfim 1838 . . . . . . . 8
87 breq1 4321 . . . . . . . . 9
88 sbceq1a 3234 . . . . . . . . 9
8987, 88imbi12d 313 . . . . . . . 8
9083, 86, 89cbval 1989 . . . . . . 7
9182, 90syl6ibr 220 . . . . . 6
925, 8, 11, 17, 91finds1 6515 . . . . 5
939219.21bi 1781 . . . 4
9493rexlimiv 2878 . . 3
952, 94sylbi 189 . 2
961, 95vtoclga 3076 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  <->wb 178  /\wa 360  A.wal 1564  E.wex 1565  =wceq 1670  e.wcel 1732  =/=wne 2652  E.wrex 2760   cvv 3015  [.wsbc 3224  \cdif 3362  u.cun 3363  C_wss 3365   c0 3673  {csn 3909   class class class wbr 4318  succsuc 4742   com 6486   cen 7270   cfn 7273
This theorem is referenced by:  findcard2s  7514  frfi  7518  fnfi  7550  iunfi  7560  finsschain  7580  infdiffi  7779  fin1a2lem10  8460  wunfi  8767  rexfiuz  12682  drsdirfi  14949  fiuncmp  18481  finiunmbl  20453  mbfresfi  27618  heibor1lem  27890  modfsummod  29426  pclfinclN  32297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1570  ax-4 1581  ax-5 1644  ax-6 1685  ax-7 1705  ax-8 1734  ax-9 1736  ax-10 1751  ax-11 1756  ax-12 1768  ax-13 1955  ax-ext 2470  ax-sep 4439  ax-nul 4447  ax-pow 4493  ax-pr 4554  ax-un 6382
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1338  df-ex 1566  df-nf 1569  df-sb 1677  df-eu 2317  df-mo 2318  df-clab 2476  df-cleq 2482  df-clel 2485  df-nfc 2614  df-ne 2654  df-ral 2764  df-rex 2765  df-rab 2768  df-v 3017  df-sbc 3225  df-dif 3368  df-un 3370  df-in 3372  df-ss 3379  df-pss 3381  df-nul 3674  df-if 3826  df-pw 3895  df-sn 3915  df-pr 3916  df-tp 3917  df-op 3918  df-uni 4118  df-br 4319  df-opab 4377  df-tr 4412  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4868  df-rel 4869  df-cnv 4870  df-co 4871  df-dm 4872  df-rn 4873  df-res 4874  df-ima 4875  df-iota 5401  df-fun 5440  df-fn 5441  df-f 5442  df-f1 5443  df-fo 5444  df-f1o 5445  df-fv 5446  df-om 6487  df-1o 6886  df-er 7067  df-en 7274  df-fin 7277
  Copyright terms: Public domain W3C validator