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

Theorem findsg 7055
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 3612 . . . . . . 7 (𝑥 = ∅ → (𝐵𝑥𝐵 ⊆ ∅))
21adantl 482 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝐵𝑥𝐵 ⊆ ∅))
3 eqeq2 2632 . . . . . . . 8 (𝐵 = ∅ → (𝑥 = 𝐵𝑥 = ∅))
4 findsg.1 . . . . . . . 8 (𝑥 = 𝐵 → (𝜑𝜓))
53, 4syl6bir 244 . . . . . . 7 (𝐵 = ∅ → (𝑥 = ∅ → (𝜑𝜓)))
65imp 445 . . . . . 6 ((𝐵 = ∅ ∧ 𝑥 = ∅) → (𝜑𝜓))
72, 6imbi12d 334 . . . . 5 ((𝐵 = ∅ ∧ 𝑥 = ∅) → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜓)))
81imbi1d 331 . . . . . 6 (𝑥 = ∅ → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ ∅ → 𝜑)))
9 ss0 3952 . . . . . . . . 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 3612 . . . . 5 (𝑥 = 𝑦 → (𝐵𝑥𝐵𝑦))
17 findsg.2 . . . . 5 (𝑥 = 𝑦 → (𝜑𝜒))
1816, 17imbi12d 334 . . . 4 (𝑥 = 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵𝑦𝜒)))
1918imbi2d 330 . . 3 (𝑥 = 𝑦 → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵𝑦𝜒))))
20 sseq2 3612 . . . . 5 (𝑥 = suc 𝑦 → (𝐵𝑥𝐵 ⊆ suc 𝑦))
21 findsg.3 . . . . 5 (𝑥 = suc 𝑦 → (𝜑𝜃))
2220, 21imbi12d 334 . . . 4 (𝑥 = suc 𝑦 → ((𝐵𝑥𝜑) ↔ (𝐵 ⊆ suc 𝑦𝜃)))
2322imbi2d 330 . . 3 (𝑥 = suc 𝑦 → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵 ⊆ suc 𝑦𝜃))))
24 sseq2 3612 . . . . 5 (𝑥 = 𝐴 → (𝐵𝑥𝐵𝐴))
25 findsg.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
2624, 25imbi12d 334 . . . 4 (𝑥 = 𝐴 → ((𝐵𝑥𝜑) ↔ (𝐵𝐴𝜏)))
2726imbi2d 330 . . 3 (𝑥 = 𝐴 → ((𝐵 ∈ ω → (𝐵𝑥𝜑)) ↔ (𝐵 ∈ ω → (𝐵𝐴𝜏))))
28 findsg.5 . . . 4 (𝐵 ∈ ω → 𝜓)
2928a1d 25 . . 3 (𝐵 ∈ ω → (𝐵 ⊆ ∅ → 𝜓))
30 vex 3193 . . . . . . . . . . . . . 14 𝑦 ∈ V
3130sucex 6973 . . . . . . . . . . . . 13 suc 𝑦 ∈ V
3231eqvinc 3318 . . . . . . . . . . . 12 (suc 𝑦 = 𝐵 ↔ ∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵))
3328, 4syl5ibr 236 . . . . . . . . . . . . . 14 (𝑥 = 𝐵 → (𝐵 ∈ ω → 𝜑))
3421biimpd 219 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝜑𝜃))
3533, 34sylan9r 689 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃))
3635exlimiv 1855 . . . . . . . . . . . 12 (∃𝑥(𝑥 = suc 𝑦𝑥 = 𝐵) → (𝐵 ∈ ω → 𝜃))
3732, 36sylbi 207 . . . . . . . . . . 11 (suc 𝑦 = 𝐵 → (𝐵 ∈ ω → 𝜃))
3837eqcoms 2629 . . . . . . . . . 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 2791 . . . . . . . . 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 7033 . . . . . . . . 9 (𝐵 ∈ ω → 𝐵 ∈ On)
48 nnon 7033 . . . . . . . . 9 (𝑦 ∈ ω → 𝑦 ∈ On)
49 onsssuc 5782 . . . . . . . . . 10 ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵𝑦𝐵 ∈ suc 𝑦))
50 suceloni 6975 . . . . . . . . . . 11 (𝑦 ∈ On → suc 𝑦 ∈ On)
51 onelpss 5733 . . . . . . . . . . 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 7054 . 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 1987  wne 2790  wss 3560  c0 3897  Oncon0 5692  suc csuc 5694  ωcom 7027
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 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877  ax-un 6914
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 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-tr 4723  df-eprel 4995  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-om 7028
This theorem is referenced by:  nnaordi  7658  inf3lem5  8489  ackbij2lem4  9024  sornom  9059  fin23lem15  9116  fin23lem36  9130  isf32lem1  9135  isf32lem2  9136  wunex2  9520  indpi  9689
  Copyright terms: Public domain W3C validator