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

Theorem findsg 7041
Description: Principle of Finite Induction (inference schema), using implicit substitutions. The first four hypotheses establish the substitutions we need. The last two are the basis and the induction step. The basis of this version is an arbitrary natural number 𝐵 instead of zero. (Contributed by NM, 16-Sep-1995.)
Hypotheses
Ref Expression
findsg.1 (𝑥 = 𝐵 → (𝜑𝜓))
findsg.2 (𝑥 = 𝑦 → (𝜑𝜒))
findsg.3 (𝑥 = suc 𝑦 → (𝜑𝜃))
findsg.4 (𝑥 = 𝐴 → (𝜑𝜏))
findsg.5 (𝐵 ∈ ω → 𝜓)
findsg.6 (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵𝑦) → (𝜒𝜃))
Assertion
Ref Expression
findsg (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵𝐴) → 𝜏)
Distinct variable groups:   𝑥,𝐴   𝑥,𝑦,𝐵   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem findsg
StepHypRef Expression
1 sseq2 3611 . . . . . . 7 (𝑥 = ∅ → (𝐵𝑥𝐵 ⊆ ∅))
21adantl 482 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵𝑥𝐵 ⊆ ∅))
3 eqeq2 2637 . . . . . . . 8 (𝐵 = ∅ → (𝑥 = 𝐵𝑥 = ∅))
4 findsg.1 . . . . . . . 8 (𝑥 = 𝐵 → (𝜑𝜓))
53, 4syl6bir 244 . . . . . . 7 (𝐵 = ∅ → (𝑥 = ∅ → (𝜑𝜓)))
65imp 445 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑𝜓))
72, 6imbi12d 334 . . . . 5 ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
81imbi1d 331 . . . . . 6 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9 ss0 3951 . . . . . . . . 9 (𝐵 ⊆ ∅ → 𝐵 = ∅)
109con3i 150 . . . . . . . 8 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅)
1110pm2.21d 118 . . . . . . 7 𝐵 = ∅ → (𝐵 ⊆ ∅ → (𝜑𝜓)))
1211pm5.74d 262 . . . . . 6 𝐵 = ∅ → ((𝐵 ⊆ ∅ → 𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
138, 12sylan9bbr 736 . . . . 5 ((¬ 𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
147, 13pm2.61ian 830 . . . 4 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
1514imbi2d 330 . . 3 (𝑥 = ∅ → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓))))
16 sseq2 3611 . . . . 5 (𝑥 = 𝑦 → (𝐵𝑥𝐵𝑦))
17 findsg.2 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜒))
1816, 17imbi12d 334 . . . 4 (𝑥 = 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵𝑦𝜒)))
1918imbi2d 330 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵𝑦𝜒))))
20 sseq2 3611 . . . . 5 (𝑥 = suc 𝑦 → (𝐵𝑥𝐵 ⊆ suc 𝑦))
21 findsg.3 . . . . 5 (𝑥 = suc 𝑦 → (𝜑𝜃))
2220, 21imbi12d 334 . . . 4 (𝑥 = suc 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ suc 𝑦𝜃)))
2322imbi2d 330 . . 3 (𝑥 = suc 𝑦 → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦𝜃))))
24 sseq2 3611 . . . . 5 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
25 findsg.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
2624, 25imbi12d 334 . . . 4 (𝑥 = 𝐴 → ((𝐵𝑥𝜑) ↔ (𝐵𝐴𝜏)))
2726imbi2d 330 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵𝐴𝜏))))
28 findsg.5 . . . 4 (𝐵 ∈ ω → 𝜓)
2928a1d 25 . . 3 (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓))
30 vex 3194 . . . . . . . . . . . . . 14 𝑦 ∈ V
3130sucex 6959 . . . . . . . . . . . . 13 suc 𝑦 ∈ V
3231eqvinc 3318 . . . . . . . . . . . 12 (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵))
3328, 4syl5ibr 236 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝐵 ∈ ω → 𝜑))
3421biimpd 219 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝜑𝜃))
3533, 34sylan9r 689 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃))
3635exlimiv 1860 . . . . . . . . . . . 12 (∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃))
3732, 36sylbi 207 . . . . . . . . . . 11 (suc 𝑦 = 𝐵 → (𝐵 ∈ ω → 𝜃))
3837eqcoms 2634 . . . . . . . . . 10 (𝐵 = suc 𝑦 → (𝐵 ∈ ω → 𝜃))
3938imim2i 16 . . . . . . . . 9 ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ ω → 𝜃)))
4039a1d 25 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦 → (𝐵 ∈ ω → 𝜃))))
4140com4r 94 . . . . . . 7 (𝐵 ∈ ω → ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
4241adantl 482 . . . . . 6 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
43 df-ne 2797 . . . . . . . . 9 (𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦)
4443anbi2i 729 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ (𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦))
45 annim 441 . . . . . . . 8 ((𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
4644, 45bitri 264 . . . . . . 7 ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) ↔ ¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦))
47 nnon 7019 . . . . . . . . 9 (𝐵 ∈ ω → 𝐵 ∈ On)
48 nnon 7019 . . . . . . . . 9 (𝑦 ∈ ω → 𝑦 ∈ On)
49 onsssuc 5775 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦𝐵 ∈ suc 𝑦))
50 suceloni 6961 . . . . . . . . . . 11 (𝑦 ∈ On → suc 𝑦 ∈ On)
51 onelpss 5726 . . . . . . . . . . 11 ((𝐵 ∈ On ∧ suc 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5250, 51sylan2 491 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 ∈ suc 𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5349, 52bitrd 268 . . . . . . . . 9 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
5447, 48, 53syl2anr 495 . . . . . . . 8 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵𝑦 ↔ (𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦)))
55 findsg.6 . . . . . . . . . . . 12 (((𝑦 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵𝑦) → (𝜒𝜃))
5655ex 450 . . . . . . . . . . 11 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵𝑦 → (𝜒𝜃)))
57 ax-1 6 . . . . . . . . . . 11 (𝜃 → (𝐵 ⊆ suc 𝑦𝜃))
5856, 57syl8 76 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵𝑦 → (𝜒 → (𝐵 ⊆ suc 𝑦𝜃))))
5958a2d 29 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵𝑦𝜒) → (𝐵𝑦 → (𝐵 ⊆ suc 𝑦𝜃))))
6059com23 86 . . . . . . . 8 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵𝑦 → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6154, 60sylbird 250 . . . . . . 7 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6246, 61syl5bir 233 . . . . . 6 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → (¬ (𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6342, 62pm2.61d 170 . . . . 5 ((𝑦 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃)))
6463ex 450 . . . 4 (𝑦 ∈ ω → (𝐵 ∈ ω → ((𝐵𝑦𝜒) → (𝐵 ⊆ suc 𝑦𝜃))))
6564a2d 29 . . 3 (𝑦 ∈ ω → ((𝐵 ∈ ω → (𝐵𝑦𝜒)) → (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦𝜃))))
6615, 19, 23, 27, 29, 65finds 7040 . 2 (𝐴 ∈ ω → (𝐵 ∈ ω → (𝐵𝐴𝜏)))
6766imp31 448 1 (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ 𝐵𝐴) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1992  wne 2796  wss 3560  c0 3896  Oncon0 5685  suc csuc 5687  ωcom 7013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6903
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-tr 4718  df-eprel 4990  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-om 7014
This theorem is referenced by:  nnaordi  7644  inf3lem5  8474  ackbij2lem4  9009  sornom  9044  fin23lem15  9101  fin23lem36  9115  isf32lem1  9120  isf32lem2  9121  wunex2  9505  indpi  9674
  Copyright terms: Public domain W3C validator