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

Theorem findcard2s 7551
Description: Variation of findcard2 7550 requiring that the element added in the induction step not be a member of the original set. (Contributed by Paul Chapman, 30-Nov-2012.)
Hypotheses
Ref Expression
findcard2s.1  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
findcard2s.2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
findcard2s.3  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
findcard2s.4  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
findcard2s.5  |-  ps
findcard2s.6  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
Assertion
Ref Expression
findcard2s  |-  ( A  e.  Fin  ->  ta )
Distinct variable groups:    x, A, y, z    ch, x    ph, y,
z    ps, x    ta, x    th, x
Allowed substitution hints:    ph( x)    ps( y, z)    ch( y, z)    th( y, z)    ta( y,
z)

Proof of Theorem findcard2s
StepHypRef Expression
1 findcard2s.1 . 2  |-  ( x  =  (/)  ->  ( ph  <->  ps ) )
2 findcard2s.2 . 2  |-  ( x  =  y  ->  ( ph 
<->  ch ) )
3 findcard2s.3 . 2  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ph  <->  th )
)
4 findcard2s.4 . 2  |-  ( x  =  A  ->  ( ph 
<->  ta ) )
5 findcard2s.5 . 2  |-  ps
6 findcard2s.6 . . . 4  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ch  ->  th ) )
76ex 434 . . 3  |-  ( y  e.  Fin  ->  ( -.  z  e.  y  ->  ( ch  ->  th )
) )
8 uncom 3498 . . . . . . 7  |-  ( { z }  u.  y
)  =  ( y  u.  { z } )
9 snssi 4015 . . . . . . . 8  |-  ( z  e.  y  ->  { z }  C_  y )
10 ssequn1 3524 . . . . . . . 8  |-  ( { z }  C_  y  <->  ( { z }  u.  y )  =  y )
119, 10sylib 196 . . . . . . 7  |-  ( z  e.  y  ->  ( { z }  u.  y )  =  y )
128, 11syl5reqr 2488 . . . . . 6  |-  ( z  e.  y  ->  y  =  ( y  u. 
{ z } ) )
13 vex 2973 . . . . . . 7  |-  y  e. 
_V
1413eqvinc 3084 . . . . . 6  |-  ( y  =  ( y  u. 
{ z } )  <->  E. x ( x  =  y  /\  x  =  ( y  u.  {
z } ) ) )
1512, 14sylib 196 . . . . 5  |-  ( z  e.  y  ->  E. x
( x  =  y  /\  x  =  ( y  u.  { z } ) ) )
162bicomd 201 . . . . . . 7  |-  ( x  =  y  ->  ( ch 
<-> 
ph ) )
1716, 3sylan9bb 699 . . . . . 6  |-  ( ( x  =  y  /\  x  =  ( y  u.  { z } ) )  ->  ( ch  <->  th ) )
1817exlimiv 1688 . . . . 5  |-  ( E. x ( x  =  y  /\  x  =  ( y  u.  {
z } ) )  ->  ( ch  <->  th )
)
1915, 18syl 16 . . . 4  |-  ( z  e.  y  ->  ( ch 
<->  th ) )
2019biimpd 207 . . 3  |-  ( z  e.  y  ->  ( ch  ->  th ) )
217, 20pm2.61d2 160 . 2  |-  ( y  e.  Fin  ->  ( ch  ->  th ) )
221, 2, 3, 4, 5, 21findcard2 7550 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756    u. cun 3324    C_ wss 3326   (/)c0 3635   {csn 3875   Fincfn 7308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3185  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-br 4291  df-opab 4349  df-tr 4384  df-eprel 4630  df-id 4634  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-om 6475  df-1o 6918  df-er 7099  df-en 7309  df-fin 7312
This theorem is referenced by:  findcard2d  7552  ac6sfi  7554  domunfican  7582  fodomfi  7588  hashxplem  12193  hashmap  12195  hashbc  12204  hashf1lem2  12207  hashf1  12208  fsum2d  13236  fsumabs  13262  fsumrlim  13272  fsumo1  13273  fsumiun  13282  incexclem  13297  gsum2dlem2  16460  gsum2dOLD  16462  ablfac1eulem  16571  mplcoe1  17542  mplcoe5  17546  mplcoe2OLD  17548  evl1gsumd  17789  mdetunilem9  18424  ptcmpfi  19384  tmdgsum  19664  fsumcn  20444  ovolfiniun  20982  volfiniun  21026  itgfsum  21302  dvmptfsum  21445  jensen  22380  gsumle  26244  gsumvsca1  26249  gsumvsca2  26250  fprod2d  27490  finixpnum  28411  pwslnm  29444  fnchoice  29748  coe1fzgsumd  30835
  Copyright terms: Public domain W3C validator