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

Theorem findcard2 7540
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  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
findcard2.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
findcard2.3  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
findcard2.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
findcard2.5  |-  ps
findcard2.6  |-  ( y  e.  Fin  ->  ( ch  ->  th ) )
Assertion
Ref Expression
findcard2  |-  ( A  e.  Fin  ->  ta )
Distinct variable groups:    x, y,
z, A    ps, x    ch, x    th, x    ta, x    ph, y, z
Allowed substitution hints:    ph( x)    ps( y, z)    ch( y, z)    th( y, z)    ta( y,
z)

Proof of Theorem findcard2
Dummy variables  w  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard2.4 . 2  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
2 isfi 7321 . . 3  |-  ( x  e.  Fin  <->  E. w  e.  om  x  ~~  w
)
3 breq2 4284 . . . . . . . 8  |-  ( w  =  (/)  ->  ( x 
~~  w  <->  x  ~~  (/) ) )
43imbi1d 317 . . . . . . 7  |-  ( w  =  (/)  ->  ( ( x  ~~  w  ->  ph )  <->  ( x  ~~  (/) 
->  ph ) ) )
54albidv 1678 . . . . . 6  |-  ( w  =  (/)  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  (/)  ->  ph )
) )
6 breq2 4284 . . . . . . . 8  |-  ( w  =  v  ->  (
x  ~~  w  <->  x  ~~  v ) )
76imbi1d 317 . . . . . . 7  |-  ( w  =  v  ->  (
( x  ~~  w  ->  ph )  <->  ( x  ~~  v  ->  ph )
) )
87albidv 1678 . . . . . 6  |-  ( w  =  v  ->  ( A. x ( x  ~~  w  ->  ph )  <->  A. x
( x  ~~  v  ->  ph ) ) )
9 breq2 4284 . . . . . . . 8  |-  ( w  =  suc  v  -> 
( x  ~~  w  <->  x 
~~  suc  v )
)
109imbi1d 317 . . . . . . 7  |-  ( w  =  suc  v  -> 
( ( x  ~~  w  ->  ph )  <->  ( x  ~~  suc  v  ->  ph )
) )
1110albidv 1678 . . . . . 6  |-  ( w  =  suc  v  -> 
( A. x ( x  ~~  w  ->  ph )  <->  A. x ( x 
~~  suc  v  ->  ph ) ) )
12 en0 7360 . . . . . . . 8  |-  ( x 
~~  (/)  <->  x  =  (/) )
13 findcard2.5 . . . . . . . . 9  |-  ps
14 findcard2.1 . . . . . . . . 9  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
1513, 14mpbiri 233 . . . . . . . 8  |-  ( x  =  (/)  ->  ph )
1612, 15sylbi 195 . . . . . . 7  |-  ( x 
~~  (/)  ->  ph )
1716ax-gen 1594 . . . . . 6  |-  A. x
( x  ~~  (/)  ->  ph )
18 nsuceq0 4786 . . . . . . . . . . . 12  |-  suc  v  =/=  (/)
19 breq1 4283 . . . . . . . . . . . . . . . 16  |-  ( w  =  (/)  ->  ( w 
~~  suc  v  <->  (/)  ~~  suc  v ) )
2019anbi2d 696 . . . . . . . . . . . . . . 15  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  <-> 
( v  e.  om  /\  (/)  ~~  suc  v ) ) )
21 peano1 6484 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
22 peano2 6485 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  om  ->  suc  v  e.  om )
23 nneneq 7482 . . . . . . . . . . . . . . . . . 18  |-  ( (
(/)  e.  om  /\  suc  v  e.  om )  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2421, 22, 23sylancr 656 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  om  ->  ( (/)  ~~  suc  v  <->  (/)  =  suc  v ) )
2524biimpa 481 . . . . . . . . . . . . . . . 16  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  (/)  =  suc  v )
2625eqcomd 2438 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  om  /\  (/)  ~~  suc  v )  ->  suc  v  =  (/) )
2720, 26syl6bi 228 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  suc  v  =  (/) ) )
2827com12 31 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =  (/)  ->  suc  v  =  (/) ) )
2928necon3d 2636 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( suc  v  =/=  (/)  ->  w  =/=  (/) ) )
3018, 29mpi 17 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  w  =/=  (/) )
3130ex 434 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  ->  w  =/=  (/) ) )
32 n0 3634 . . . . . . . . . . . 12  |-  ( w  =/=  (/)  <->  E. z  z  e.  w )
33 dif1en 7533 . . . . . . . . . . . . . . 15  |-  ( ( v  e.  om  /\  w  ~~  suc  v  /\  z  e.  w )  ->  ( w  \  {
z } )  ~~  v )
34333expia 1182 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( w  \  { z } ) 
~~  v ) )
35 snssi 4005 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  w  ->  { z }  C_  w )
36 uncom 3488 . . . . . . . . . . . . . . . . . . 19  |-  ( ( w  \  { z } )  u.  {
z } )  =  ( { z }  u.  ( w  \  { z } ) )
37 undif 3747 . . . . . . . . . . . . . . . . . . . 20  |-  ( { z }  C_  w  <->  ( { z }  u.  ( w  \  { z } ) )  =  w )
3837biimpi 194 . . . . . . . . . . . . . . . . . . 19  |-  ( { z }  C_  w  ->  ( { z }  u.  ( w  \  { z } ) )  =  w )
3936, 38syl5eq 2477 . . . . . . . . . . . . . . . . . 18  |-  ( { z }  C_  w  ->  ( ( w  \  { z } )  u.  { z } )  =  w )
40 vex 2965 . . . . . . . . . . . . . . . . . . . . 21  |-  w  e. 
_V
41 difexg 4428 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  e.  _V  ->  (
w  \  { z } )  e.  _V )
4240, 41ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  ( w 
\  { z } )  e.  _V
43 breq1 4283 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( y  ~~  v 
<->  ( w  \  {
z } )  ~~  v ) )
4443anbi2d 696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( ( v  e.  om  /\  y  ~~  v )  <->  ( v  e.  om  /\  ( w 
\  { z } )  ~~  v ) ) )
45 uneq1 3491 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( w  \  { z } )  ->  ( y  u. 
{ z } )  =  ( ( w 
\  { z } )  u.  { z } ) )
46 dfsbcq 3177 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  u.  { z } )  =  ( ( w  \  {
z } )  u. 
{ z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
4745, 46syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( w  \  { z } )  ->  ( [. (
y  u.  { z } )  /  x ]. ph  <->  [. ( ( w 
\  { z } )  u.  { z } )  /  x ]. ph ) )
4847imbi2d 316 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  =  ( w  \  { z } )  ->  ( ( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph )  <->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
) )
4944, 48imbi12d 320 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  =  ( w  \  { z } )  ->  ( ( ( v  e.  om  /\  y  ~~  v )  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )  <->  ( (
v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
) ) )
50 breq1 4283 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  (
x  ~~  v  <->  y  ~~  v ) )
51 findcard2.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
5250, 51imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  y  ->  (
( x  ~~  v  ->  ph )  <->  ( y  ~~  v  ->  ch )
) )
5352spv 1954 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. x ( x  ~~  v  ->  ph )  ->  (
y  ~~  v  ->  ch ) )
54 rspe 2767 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  om  /\  y  ~~  v )  ->  E. v  e.  om  y  ~~  v )
55 isfi 7321 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  Fin  <->  E. v  e.  om  y  ~~  v
)
5654, 55sylibr 212 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
y  e.  Fin )
57 pm2.27 39 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y 
~~  v  ->  (
( y  ~~  v  ->  ch )  ->  ch ) )
5857adantl 463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  ch ) )
59 findcard2.6 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  Fin  ->  ( ch  ->  th ) )
6056, 58, 59sylsyld 56 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( ( y  ~~  v  ->  ch )  ->  th ) )
6153, 60syl5 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( A. x ( x  ~~  v  ->  ph )  ->  th )
)
62 vex 2965 . . . . . . . . . . . . . . . . . . . . . . 23  |-  y  e. 
_V
63 snex 4521 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { z }  e.  _V
6462, 63unex 6367 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  u.  { z } )  e.  _V
65 findcard2.3 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
6664, 65sbcie 3209 . . . . . . . . . . . . . . . . . . . . 21  |-  ( [. ( y  u.  {
z } )  /  x ]. ph  <->  th )
6761, 66syl6ibr 227 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( v  e.  om  /\  y  ~~  v )  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. (
y  u.  { z } )  /  x ]. ph ) )
6842, 49, 67vtocl 3013 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v  e.  om  /\  ( w  \  { z } )  ~~  v
)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )
)
69 dfsbcq 3177 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  ( [. ( ( w  \  { z } )  u.  { z } )  /  x ]. ph  <->  [. w  /  x ]. ph ) )
7069imbi2d 316 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  (
( A. x ( x  ~~  v  ->  ph )  ->  [. (
( w  \  {
z } )  u. 
{ z } )  /  x ]. ph )  <->  ( A. x ( x 
~~  v  ->  ph )  ->  [. w  /  x ]. ph ) ) )
7168, 70syl5ib 219 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  \  {
z } )  u. 
{ z } )  =  w  ->  (
( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
7235, 39, 713syl 20 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  w  ->  (
( v  e.  om  /\  ( w  \  {
z } )  ~~  v )  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
7372exp3a 436 . . . . . . . . . . . . . . . 16  |-  ( z  e.  w  ->  (
v  e.  om  ->  ( ( w  \  {
z } )  ~~  v  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
7473com12 31 . . . . . . . . . . . . . . 15  |-  ( v  e.  om  ->  (
z  e.  w  -> 
( ( w  \  { z } ) 
~~  v  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
7574adantr 462 . . . . . . . . . . . . . 14  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( (
w  \  { z } )  ~~  v  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
7634, 75mpdd 40 . . . . . . . . . . . . 13  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( z  e.  w  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
7776exlimdv 1689 . . . . . . . . . . . 12  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( E. z 
z  e.  w  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
7832, 77syl5bi 217 . . . . . . . . . . 11  |-  ( ( v  e.  om  /\  w  ~~  suc  v )  ->  ( w  =/=  (/)  ->  ( A. x
( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
7978ex 434 . . . . . . . . . 10  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( w  =/=  (/)  ->  ( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) ) )
8031, 79mpdd 40 . . . . . . . . 9  |-  ( v  e.  om  ->  (
w  ~~  suc  v  -> 
( A. x ( x  ~~  v  ->  ph )  ->  [. w  /  x ]. ph )
) )
8180com23 78 . . . . . . . 8  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  (
w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
8281alrimdv 1686 . . . . . . 7  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. w
( w  ~~  suc  v  ->  [. w  /  x ]. ph ) ) )
83 nfv 1672 . . . . . . . 8  |-  F/ w
( x  ~~  suc  v  ->  ph )
84 nfv 1672 . . . . . . . . 9  |-  F/ x  w  ~~  suc  v
85 nfsbc1v 3194 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
8684, 85nfim 1851 . . . . . . . 8  |-  F/ x
( w  ~~  suc  v  ->  [. w  /  x ]. ph )
87 breq1 4283 . . . . . . . . 9  |-  ( x  =  w  ->  (
x  ~~  suc  v  <->  w  ~~  suc  v ) )
88 sbceq1a 3185 . . . . . . . . 9  |-  ( x  =  w  ->  ( ph 
<-> 
[. w  /  x ]. ph ) )
8987, 88imbi12d 320 . . . . . . . 8  |-  ( x  =  w  ->  (
( x  ~~  suc  v  ->  ph )  <->  ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
) )
9083, 86, 89cbval 1968 . . . . . . 7  |-  ( A. x ( x  ~~  suc  v  ->  ph )  <->  A. w ( w  ~~  suc  v  ->  [. w  /  x ]. ph )
)
9182, 90syl6ibr 227 . . . . . 6  |-  ( v  e.  om  ->  ( A. x ( x  ~~  v  ->  ph )  ->  A. x
( x  ~~  suc  v  ->  ph ) ) )
925, 8, 11, 17, 91finds1 6494 . . . . 5  |-  ( w  e.  om  ->  A. x
( x  ~~  w  ->  ph ) )
939219.21bi 1803 . . . 4  |-  ( w  e.  om  ->  (
x  ~~  w  ->  ph ) )
9493rexlimiv 2825 . . 3  |-  ( E. w  e.  om  x  ~~  w  ->  ph )
952, 94sylbi 195 . 2  |-  ( x  e.  Fin  ->  ph )
961, 95vtoclga 3025 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1360    = wceq 1362   E.wex 1589    e. wcel 1755    =/= wne 2596   E.wrex 2706   _Vcvv 2962   [.wsbc 3175    \ cdif 3313    u. cun 3314    C_ wss 3316   (/)c0 3625   {csn 3865   class class class wbr 4280   suc csuc 4708   omcom 6465    ~~ cen 7295   Fincfn 7298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-om 6466  df-1o 6908  df-er 7089  df-en 7299  df-fin 7302
This theorem is referenced by:  findcard2s  7541  frfi  7545  fnfi  7577  iunfi  7587  finsschain  7606  infdiffi  7851  fin1a2lem10  8566  wunfi  8875  rexfiuz  12818  drsdirfi  15090  fiuncmp  18848  finiunmbl  20866  mbfresfi  28279  heibor1lem  28549  modfsummod  30088  pclfinclN  33164
  Copyright terms: Public domain W3C validator