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 ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → 𝜏 )