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

Theorem findcard2s 7773
Description: Variation of findcard2 7772 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 3653 . . . . . . 7  |-  ( { z }  u.  y
)  =  ( y  u.  { z } )
9 snssi 4177 . . . . . . . 8  |-  ( z  e.  y  ->  { z }  C_  y )
10 ssequn1 3679 . . . . . . . 8  |-  ( { z }  C_  y  <->  ( { z }  u.  y )  =  y )
119, 10sylib 196 . . . . . . 7  |-  ( z  e.  y  ->  ( { z }  u.  y )  =  y )
128, 11syl5reqr 2523 . . . . . 6  |-  ( z  e.  y  ->  y  =  ( y  u. 
{ z } ) )
13 vex 3121 . . . . . . 7  |-  y  e. 
_V
1413eqvinc 3235 . . . . . 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 1698 . . . . 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 7772 1  |-  ( A  e.  Fin  ->  ta )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767    u. cun 3479    C_ wss 3481   (/)c0 3790   {csn 4033   Fincfn 7528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-om 6696  df-1o 7142  df-er 7323  df-en 7529  df-fin 7532
This theorem is referenced by:  findcard2d  7774  ac6sfi  7776  domunfican  7805  fodomfi  7811  hashxplem  12472  hashmap  12474  hashbc  12483  hashf1lem2  12486  hashf1  12487  fsum2d  13566  fsumabs  13595  fsumrlim  13605  fsumo1  13606  fsumiun  13615  incexclem  13628  gsum2dlem2  16871  gsum2dOLD  16873  ablfac1eulem  16995  mplcoe1  17997  mplcoe5  18001  mplcoe2OLD  18003  coe1fzgsumd  18214  evl1gsumd  18263  mdetunilem9  18991  ptcmpfi  20182  tmdgsum  20462  fsumcn  21242  ovolfiniun  21780  volfiniun  21825  itgfsum  22101  dvmptfsum  22244  jensen  23184  gsumle  27595  gsumvsca1  27598  gsumvsca2  27599  fprod2d  29038  finixpnum  29965  pwslnm  30968  fnchoice  31306
  Copyright terms: Public domain W3C validator