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

Theorem findcard 9196
Description: Schema for induction on the cardinality of a finite set. The inductive hypothesis is that the result is true on the given set with any one element removed. The result is then proven to be true for all finite sets. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
findcard.1 (𝑥 = ∅ → (𝜑𝜓))
findcard.2 (𝑥 = (𝑦 ∖ {𝑧}) → (𝜑𝜒))
findcard.3 (𝑥 = 𝑦 → (𝜑𝜃))
findcard.4 (𝑥 = 𝐴 → (𝜑𝜏))
findcard.5 𝜓
findcard.6 (𝑦 ∈ Fin → (∀𝑧𝑦 𝜒𝜃))
Assertion
Ref Expression
findcard (𝐴 ∈ Fin → 𝜏)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦,𝑧)   𝜒(𝑦,𝑧)   𝜃(𝑦,𝑧)   𝜏(𝑦,𝑧)

Proof of Theorem findcard
Dummy variables 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 findcard.4 . 2 (𝑥 = 𝐴 → (𝜑𝜏))
2 isfi 9005 . . 3 (𝑥 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑥𝑤)
3 breq2 5156 . . . . . . . 8 (𝑤 = ∅ → (𝑥𝑤𝑥 ≈ ∅))
43imbi1d 340 . . . . . . 7 (𝑤 = ∅ → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ ∅ → 𝜑)))
54albidv 1915 . . . . . 6 (𝑤 = ∅ → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ ∅ → 𝜑)))
6 breq2 5156 . . . . . . . 8 (𝑤 = 𝑣 → (𝑥𝑤𝑥𝑣))
76imbi1d 340 . . . . . . 7 (𝑤 = 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥𝑣𝜑)))
87albidv 1915 . . . . . 6 (𝑤 = 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥𝑣𝜑)))
9 breq2 5156 . . . . . . . 8 (𝑤 = suc 𝑣 → (𝑥𝑤𝑥 ≈ suc 𝑣))
109imbi1d 340 . . . . . . 7 (𝑤 = suc 𝑣 → ((𝑥𝑤𝜑) ↔ (𝑥 ≈ suc 𝑣𝜑)))
1110albidv 1915 . . . . . 6 (𝑤 = suc 𝑣 → (∀𝑥(𝑥𝑤𝜑) ↔ ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
12 en0 9046 . . . . . . . 8 (𝑥 ≈ ∅ ↔ 𝑥 = ∅)
13 findcard.5 . . . . . . . . 9 𝜓
14 findcard.1 . . . . . . . . 9 (𝑥 = ∅ → (𝜑𝜓))
1513, 14mpbiri 257 . . . . . . . 8 (𝑥 = ∅ → 𝜑)
1612, 15sylbi 216 . . . . . . 7 (𝑥 ≈ ∅ → 𝜑)
1716ax-gen 1789 . . . . . 6 𝑥(𝑥 ≈ ∅ → 𝜑)
18 peano2 7904 . . . . . . . . . . . . 13 (𝑣 ∈ ω → suc 𝑣 ∈ ω)
19 breq2 5156 . . . . . . . . . . . . . 14 (𝑤 = suc 𝑣 → (𝑦𝑤𝑦 ≈ suc 𝑣))
2019rspcev 3611 . . . . . . . . . . . . 13 ((suc 𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) → ∃𝑤 ∈ ω 𝑦𝑤)
2118, 20sylan 578 . . . . . . . . . . . 12 ((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) → ∃𝑤 ∈ ω 𝑦𝑤)
22 isfi 9005 . . . . . . . . . . . 12 (𝑦 ∈ Fin ↔ ∃𝑤 ∈ ω 𝑦𝑤)
2321, 22sylibr 233 . . . . . . . . . . 11 ((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) → 𝑦 ∈ Fin)
24233adant2 1128 . . . . . . . . . 10 ((𝑣 ∈ ω ∧ ∀𝑥(𝑥𝑣𝜑) ∧ 𝑦 ≈ suc 𝑣) → 𝑦 ∈ Fin)
25 dif1ennn 9194 . . . . . . . . . . . . . . . 16 ((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣𝑧𝑦) → (𝑦 ∖ {𝑧}) ≈ 𝑣)
26253expa 1115 . . . . . . . . . . . . . . 15 (((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) ∧ 𝑧𝑦) → (𝑦 ∖ {𝑧}) ≈ 𝑣)
27 vex 3477 . . . . . . . . . . . . . . . . 17 𝑦 ∈ V
2827difexi 5334 . . . . . . . . . . . . . . . 16 (𝑦 ∖ {𝑧}) ∈ V
29 breq1 5155 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑦 ∖ {𝑧}) → (𝑥𝑣 ↔ (𝑦 ∖ {𝑧}) ≈ 𝑣))
30 findcard.2 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑦 ∖ {𝑧}) → (𝜑𝜒))
3129, 30imbi12d 343 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑦 ∖ {𝑧}) → ((𝑥𝑣𝜑) ↔ ((𝑦 ∖ {𝑧}) ≈ 𝑣𝜒)))
3228, 31spcv 3594 . . . . . . . . . . . . . . 15 (∀𝑥(𝑥𝑣𝜑) → ((𝑦 ∖ {𝑧}) ≈ 𝑣𝜒))
3326, 32syl5com 31 . . . . . . . . . . . . . 14 (((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) ∧ 𝑧𝑦) → (∀𝑥(𝑥𝑣𝜑) → 𝜒))
3433ralrimdva 3151 . . . . . . . . . . . . 13 ((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) → (∀𝑥(𝑥𝑣𝜑) → ∀𝑧𝑦 𝜒))
3534imp 405 . . . . . . . . . . . 12 (((𝑣 ∈ ω ∧ 𝑦 ≈ suc 𝑣) ∧ ∀𝑥(𝑥𝑣𝜑)) → ∀𝑧𝑦 𝜒)
3635an32s 650 . . . . . . . . . . 11 (((𝑣 ∈ ω ∧ ∀𝑥(𝑥𝑣𝜑)) ∧ 𝑦 ≈ suc 𝑣) → ∀𝑧𝑦 𝜒)
37363impa 1107 . . . . . . . . . 10 ((𝑣 ∈ ω ∧ ∀𝑥(𝑥𝑣𝜑) ∧ 𝑦 ≈ suc 𝑣) → ∀𝑧𝑦 𝜒)
38 findcard.6 . . . . . . . . . 10 (𝑦 ∈ Fin → (∀𝑧𝑦 𝜒𝜃))
3924, 37, 38sylc 65 . . . . . . . . 9 ((𝑣 ∈ ω ∧ ∀𝑥(𝑥𝑣𝜑) ∧ 𝑦 ≈ suc 𝑣) → 𝜃)
40393exp 1116 . . . . . . . 8 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → (𝑦 ≈ suc 𝑣𝜃)))
4140alrimdv 1924 . . . . . . 7 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑦(𝑦 ≈ suc 𝑣𝜃)))
42 breq1 5155 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥 ≈ suc 𝑣𝑦 ≈ suc 𝑣))
43 findcard.3 . . . . . . . . 9 (𝑥 = 𝑦 → (𝜑𝜃))
4442, 43imbi12d 343 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥 ≈ suc 𝑣𝜑) ↔ (𝑦 ≈ suc 𝑣𝜃)))
4544cbvalvw 2031 . . . . . . 7 (∀𝑥(𝑥 ≈ suc 𝑣𝜑) ↔ ∀𝑦(𝑦 ≈ suc 𝑣𝜃))
4641, 45imbitrrdi 251 . . . . . 6 (𝑣 ∈ ω → (∀𝑥(𝑥𝑣𝜑) → ∀𝑥(𝑥 ≈ suc 𝑣𝜑)))
475, 8, 11, 17, 46finds1 7915 . . . . 5 (𝑤 ∈ ω → ∀𝑥(𝑥𝑤𝜑))
484719.21bi 2177 . . . 4 (𝑤 ∈ ω → (𝑥𝑤𝜑))
4948rexlimiv 3145 . . 3 (∃𝑤 ∈ ω 𝑥𝑤𝜑)
502, 49sylbi 216 . 2 (𝑥 ∈ Fin → 𝜑)
511, 50vtoclga 3565 1 (𝐴 ∈ Fin → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084  wal 1531   = wceq 1533  wcel 2098  wral 3058  wrex 3067  cdif 3946  c0 4326  {csn 4632   class class class wbr 5152  suc csuc 6376  ωcom 7878  cen 8969  Fincfn 8972
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433  ax-un 7748
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-om 7879  df-en 8973  df-fin 8976
This theorem is referenced by:  xpfiOLD  9352
  Copyright terms: Public domain W3C validator