This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrrdi ⊢ ( 𝐵 = ∅ → ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) ) )
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 imbitrrid ⊢ ( 𝑥 = 𝐵 → ( 𝐵 ∈ ω → 𝜑 ) )
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 onsuc ⊢ ( 𝑦 ∈ 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 biimtrrid ⊢ ( ( 𝑦 ∈ ω ∧ 𝐵 ∈ ω ) → ( ¬ ( 𝐵 ⊆ 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 ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → 𝜏 )