Metamath Proof Explorer


Theorem findsg

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 B instead of zero. (Contributed by NM, 16-Sep-1995)

Ref Expression
Hypotheses findsg.1 ( 𝑥 = 𝐵 → ( 𝜑𝜓 ) )
findsg.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
findsg.3 ( 𝑥 = suc 𝑦 → ( 𝜑𝜃 ) )
findsg.4 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
findsg.5 ( 𝐵 ∈ ω → 𝜓 )
findsg.6 ( ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵𝑦 ) → ( 𝜒𝜃 ) )
Assertion findsg ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵𝐴 ) → 𝜏 )

Proof

Step Hyp Ref Expression
1 findsg.1 ( 𝑥 = 𝐵 → ( 𝜑𝜓 ) )
2 findsg.2 ( 𝑥 = 𝑦 → ( 𝜑𝜒 ) )
3 findsg.3 ( 𝑥 = suc 𝑦 → ( 𝜑𝜃 ) )
4 findsg.4 ( 𝑥 = 𝐴 → ( 𝜑𝜏 ) )
5 findsg.5 ( 𝐵 ∈ ω → 𝜓 )
6 findsg.6 ( ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵𝑦 ) → ( 𝜒𝜃 ) )
7 sseq2 ( 𝑥 = ∅ → ( 𝐵𝑥𝐵 ⊆ ∅ ) )
8 7 adantl ( ( 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( 𝐵𝑥𝐵 ⊆ ∅ ) )
9 eqeq2 ( 𝐵 = ∅ → ( 𝑥 = 𝐵𝑥 = ∅ ) )
10 9 1 syl6bir ( 𝐵 = ∅ → ( 𝑥 = ∅ → ( 𝜑𝜓 ) ) )
11 10 imp ( ( 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( 𝜑𝜓 ) )
12 8 11 imbi12d ( ( 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
13 7 imbi1d ( 𝑥 = ∅ → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜑 ) ) )
14 ss0 ( 𝐵 ⊆ ∅ → 𝐵 = ∅ )
15 14 con3i ( ¬ 𝐵 = ∅ → ¬ 𝐵 ⊆ ∅ )
16 15 pm2.21d ( ¬ 𝐵 = ∅ → ( 𝐵 ⊆ ∅ → ( 𝜑𝜓 ) ) )
17 16 pm5.74d ( ¬ 𝐵 = ∅ → ( ( 𝐵 ⊆ ∅ → 𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
18 13 17 sylan9bbr ( ( ¬ 𝐵 = ∅ ∧ 𝑥 = ∅ ) → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
19 12 18 pm2.61ian ( 𝑥 = ∅ → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵 ⊆ ∅ → 𝜓 ) ) )
20 19 imbi2d ( 𝑥 = ∅ → ( ( 𝐵 ∈ ω → ( 𝐵𝑥𝜑 ) ) ↔ ( 𝐵 ∈ ω → ( 𝐵 ⊆ ∅ → 𝜓 ) ) ) )
21 sseq2 ( 𝑥 = 𝑦 → ( 𝐵𝑥𝐵𝑦 ) )
22 21 2 imbi12d ( 𝑥 = 𝑦 → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵𝑦𝜒 ) ) )
23 22 imbi2d ( 𝑥 = 𝑦 → ( ( 𝐵 ∈ ω → ( 𝐵𝑥𝜑 ) ) ↔ ( 𝐵 ∈ ω → ( 𝐵𝑦𝜒 ) ) ) )
24 sseq2 ( 𝑥 = suc 𝑦 → ( 𝐵𝑥𝐵 ⊆ suc 𝑦 ) )
25 24 3 imbi12d ( 𝑥 = suc 𝑦 → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵 ⊆ suc 𝑦𝜃 ) ) )
26 25 imbi2d ( 𝑥 = suc 𝑦 → ( ( 𝐵 ∈ ω → ( 𝐵𝑥𝜑 ) ) ↔ ( 𝐵 ∈ ω → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
27 sseq2 ( 𝑥 = 𝐴 → ( 𝐵𝑥𝐵𝐴 ) )
28 27 4 imbi12d ( 𝑥 = 𝐴 → ( ( 𝐵𝑥𝜑 ) ↔ ( 𝐵𝐴𝜏 ) ) )
29 28 imbi2d ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ ω → ( 𝐵𝑥𝜑 ) ) ↔ ( 𝐵 ∈ ω → ( 𝐵𝐴𝜏 ) ) ) )
30 5 a1d ( 𝐵 ∈ ω → ( 𝐵 ⊆ ∅ → 𝜓 ) )
31 vex 𝑦 ∈ V
32 31 sucex suc 𝑦 ∈ V
33 32 eqvinc ( suc 𝑦 = 𝐵 ↔ ∃ 𝑥 ( 𝑥 = suc 𝑦𝑥 = 𝐵 ) )
34 5 1 syl5ibr ( 𝑥 = 𝐵 → ( 𝐵 ∈ ω → 𝜑 ) )
35 3 biimpd ( 𝑥 = suc 𝑦 → ( 𝜑𝜃 ) )
36 34 35 sylan9r ( ( 𝑥 = suc 𝑦𝑥 = 𝐵 ) → ( 𝐵 ∈ ω → 𝜃 ) )
37 36 exlimiv ( ∃ 𝑥 ( 𝑥 = suc 𝑦𝑥 = 𝐵 ) → ( 𝐵 ∈ ω → 𝜃 ) )
38 33 37 sylbi ( suc 𝑦 = 𝐵 → ( 𝐵 ∈ ω → 𝜃 ) )
39 38 eqcoms ( 𝐵 = suc 𝑦 → ( 𝐵 ∈ ω → 𝜃 ) )
40 39 imim2i ( ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) → ( 𝐵 ⊆ suc 𝑦 → ( 𝐵 ∈ ω → 𝜃 ) ) )
41 40 a1d ( ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦 → ( 𝐵 ∈ ω → 𝜃 ) ) ) )
42 41 com4r ( 𝐵 ∈ ω → ( ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
43 42 adantl ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
44 df-ne ( 𝐵 ≠ suc 𝑦 ↔ ¬ 𝐵 = suc 𝑦 )
45 44 anbi2i ( ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) ↔ ( 𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦 ) )
46 annim ( ( 𝐵 ⊆ suc 𝑦 ∧ ¬ 𝐵 = suc 𝑦 ) ↔ ¬ ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) )
47 45 46 bitri ( ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) ↔ ¬ ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) )
48 nnon ( 𝐵 ∈ ω → 𝐵 ∈ On )
49 nnon ( 𝑦 ∈ ω → 𝑦 ∈ On )
50 onsssuc ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵𝑦𝐵 ∈ suc 𝑦 ) )
51 suceloni ( 𝑦 ∈ On → suc 𝑦 ∈ On )
52 onelpss ( ( 𝐵 ∈ On ∧ suc 𝑦 ∈ On ) → ( 𝐵 ∈ suc 𝑦 ↔ ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) ) )
53 51 52 sylan2 ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵 ∈ suc 𝑦 ↔ ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) ) )
54 50 53 bitrd ( ( 𝐵 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐵𝑦 ↔ ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) ) )
55 48 49 54 syl2anr ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝑦 ↔ ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) ) )
56 6 ex ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝑦 → ( 𝜒𝜃 ) ) )
57 56 a1ddd ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝑦 → ( 𝜒 → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
58 57 a2d ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵𝑦 → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
59 58 com23 ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵𝑦 → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
60 55 59 sylbird ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵 ⊆ suc 𝑦𝐵 ≠ suc 𝑦 ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
61 47 60 syl5bir ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ¬ ( 𝐵 ⊆ suc 𝑦𝐵 = suc 𝑦 ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
62 43 61 pm2.61d ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) )
63 62 ex ( 𝑦 ∈ ω → ( 𝐵 ∈ ω → ( ( 𝐵𝑦𝜒 ) → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
64 63 a2d ( 𝑦 ∈ ω → ( ( 𝐵 ∈ ω → ( 𝐵𝑦𝜒 ) ) → ( 𝐵 ∈ ω → ( 𝐵 ⊆ suc 𝑦𝜃 ) ) ) )
65 20 23 26 29 30 64 finds ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝐵𝐴𝜏 ) ) )
66 65 imp31 ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵𝐴 ) → 𝜏 )