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

Theorem findcard2s 8747
Description: Variation of findcard2 8746 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 (𝑥 = ∅ → (𝜑𝜓))
findcard2s.2 (𝑥 = 𝑦 → (𝜑𝜒))
findcard2s.3 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
findcard2s.4 (𝑥 = 𝐴 → (𝜑𝜏))
findcard2s.5 𝜓
findcard2s.6 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
Assertion
Ref Expression
findcard2s (𝐴 ∈ Fin → 𝜏)
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝜒,𝑥   𝜑,𝑦,𝑧   𝜓,𝑥   𝜏,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard2s
StepHypRef Expression
1 findcard2s.1 . 2 (𝑥 = ∅ → (𝜑𝜓))
2 findcard2s.2 . 2 (𝑥 = 𝑦 → (𝜑𝜒))
3 findcard2s.3 . 2 (𝑥 = (𝑦 ∪ {𝑧}) → (𝜑𝜃))
4 findcard2s.4 . 2 (𝑥 = 𝐴 → (𝜑𝜏))
5 findcard2s.5 . 2 𝜓
6 findcard2s.6 . . . 4 ((𝑦 ∈ Fin ∧ ¬ 𝑧𝑦) → (𝜒𝜃))
76ex 413 . . 3 (𝑦 ∈ Fin → (¬ 𝑧𝑦 → (𝜒𝜃)))
8 uncom 4126 . . . . . . 7 ({𝑧} ∪ 𝑦) = (𝑦 ∪ {𝑧})
9 snssi 4733 . . . . . . . 8 (𝑧𝑦 → {𝑧} ⊆ 𝑦)
10 ssequn1 4153 . . . . . . . 8 ({𝑧} ⊆ 𝑦 ↔ ({𝑧} ∪ 𝑦) = 𝑦)
119, 10sylib 219 . . . . . . 7 (𝑧𝑦 → ({𝑧} ∪ 𝑦) = 𝑦)
128, 11syl5reqr 2868 . . . . . 6 (𝑧𝑦𝑦 = (𝑦 ∪ {𝑧}))
13 vex 3495 . . . . . . 7 𝑦 ∈ V
1413eqvinc 3639 . . . . . 6 (𝑦 = (𝑦 ∪ {𝑧}) ↔ ∃𝑥(𝑥 = 𝑦𝑥 = (𝑦 ∪ {𝑧})))
1512, 14sylib 219 . . . . 5 (𝑧𝑦 → ∃𝑥(𝑥 = 𝑦𝑥 = (𝑦 ∪ {𝑧})))
162bicomd 224 . . . . . . 7 (𝑥 = 𝑦 → (𝜒𝜑))
1716, 3sylan9bb 510 . . . . . 6 ((𝑥 = 𝑦𝑥 = (𝑦 ∪ {𝑧})) → (𝜒𝜃))
1817exlimiv 1922 . . . . 5 (∃𝑥(𝑥 = 𝑦𝑥 = (𝑦 ∪ {𝑧})) → (𝜒𝜃))
1915, 18syl 17 . . . 4 (𝑧𝑦 → (𝜒𝜃))
2019biimpd 230 . . 3 (𝑧𝑦 → (𝜒𝜃))
217, 20pm2.61d2 182 . 2 (𝑦 ∈ Fin → (𝜒𝜃))
221, 2, 3, 4, 5, 21findcard2 8746 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wex 1771  wcel 2105  cun 3931  wss 3933  c0 4288  {csn 4557  Fincfn 8497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-om 7570  df-1o 8091  df-er 8278  df-en 8498  df-fin 8501
This theorem is referenced by:  findcard2d  8748  ac6sfi  8750  domunfican  8779  fodomfi  8785  hashxplem  13782  hashmap  13784  hashbc  13799  hashf1lem2  13802  hashf1  13803  fsum2d  15114  fsumabs  15144  fsumrlim  15154  fsumo1  15155  fsumiun  15164  incexclem  15179  fprod2d  15323  coprmprod  15993  coprmproddvds  15995  gsum2dlem2  19020  ablfac1eulem  19123  mplcoe1  20174  mplcoe5  20177  coe1fzgsumd  20398  evl1gsumd  20448  mdetunilem9  21157  ptcmpfi  22349  tmdgsum  22631  fsumcn  23405  ovolfiniun  24029  volfiniun  24075  itgfsum  24354  dvmptfsum  24499  jensen  25493  gsumle  30652  gsumvsca1  30781  gsumvsca2  30782  finixpnum  34758  matunitlindflem1  34769  pwslnm  39572  fnchoice  41163  dvmptfprod  42106
  Copyright terms: Public domain W3C validator