# 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 ${⊢}{x}={B}\to \left({\phi }↔{\psi }\right)$
findsg.2 ${⊢}{x}={y}\to \left({\phi }↔{\chi }\right)$
findsg.3 ${⊢}{x}=\mathrm{suc}{y}\to \left({\phi }↔{\theta }\right)$
findsg.4 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
findsg.5 ${⊢}{B}\in \mathrm{\omega }\to {\psi }$
findsg.6 ${⊢}\left(\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {y}\right)\to \left({\chi }\to {\theta }\right)$
Assertion findsg ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {A}\right)\to {\tau }$

### Proof

Step Hyp Ref Expression
1 findsg.1 ${⊢}{x}={B}\to \left({\phi }↔{\psi }\right)$
2 findsg.2 ${⊢}{x}={y}\to \left({\phi }↔{\chi }\right)$
3 findsg.3 ${⊢}{x}=\mathrm{suc}{y}\to \left({\phi }↔{\theta }\right)$
4 findsg.4 ${⊢}{x}={A}\to \left({\phi }↔{\tau }\right)$
5 findsg.5 ${⊢}{B}\in \mathrm{\omega }\to {\psi }$
6 findsg.6 ${⊢}\left(\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {y}\right)\to \left({\chi }\to {\theta }\right)$
7 sseq2 ${⊢}{x}=\varnothing \to \left({B}\subseteq {x}↔{B}\subseteq \varnothing \right)$
8 7 adantl ${⊢}\left({B}=\varnothing \wedge {x}=\varnothing \right)\to \left({B}\subseteq {x}↔{B}\subseteq \varnothing \right)$
9 eqeq2 ${⊢}{B}=\varnothing \to \left({x}={B}↔{x}=\varnothing \right)$
10 9 1 syl6bir ${⊢}{B}=\varnothing \to \left({x}=\varnothing \to \left({\phi }↔{\psi }\right)\right)$
11 10 imp ${⊢}\left({B}=\varnothing \wedge {x}=\varnothing \right)\to \left({\phi }↔{\psi }\right)$
12 8 11 imbi12d ${⊢}\left({B}=\varnothing \wedge {x}=\varnothing \right)\to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq \varnothing \to {\psi }\right)\right)$
13 7 imbi1d ${⊢}{x}=\varnothing \to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq \varnothing \to {\phi }\right)\right)$
14 ss0 ${⊢}{B}\subseteq \varnothing \to {B}=\varnothing$
15 14 con3i ${⊢}¬{B}=\varnothing \to ¬{B}\subseteq \varnothing$
16 15 pm2.21d ${⊢}¬{B}=\varnothing \to \left({B}\subseteq \varnothing \to \left({\phi }↔{\psi }\right)\right)$
17 16 pm5.74d ${⊢}¬{B}=\varnothing \to \left(\left({B}\subseteq \varnothing \to {\phi }\right)↔\left({B}\subseteq \varnothing \to {\psi }\right)\right)$
18 13 17 sylan9bbr ${⊢}\left(¬{B}=\varnothing \wedge {x}=\varnothing \right)\to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq \varnothing \to {\psi }\right)\right)$
19 12 18 pm2.61ian ${⊢}{x}=\varnothing \to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq \varnothing \to {\psi }\right)\right)$
20 19 imbi2d ${⊢}{x}=\varnothing \to \left(\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {x}\to {\phi }\right)\right)↔\left({B}\in \mathrm{\omega }\to \left({B}\subseteq \varnothing \to {\psi }\right)\right)\right)$
21 sseq2 ${⊢}{x}={y}\to \left({B}\subseteq {x}↔{B}\subseteq {y}\right)$
22 21 2 imbi12d ${⊢}{x}={y}\to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq {y}\to {\chi }\right)\right)$
23 22 imbi2d ${⊢}{x}={y}\to \left(\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {x}\to {\phi }\right)\right)↔\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {y}\to {\chi }\right)\right)\right)$
24 sseq2 ${⊢}{x}=\mathrm{suc}{y}\to \left({B}\subseteq {x}↔{B}\subseteq \mathrm{suc}{y}\right)$
25 24 3 imbi12d ${⊢}{x}=\mathrm{suc}{y}\to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)$
26 25 imbi2d ${⊢}{x}=\mathrm{suc}{y}\to \left(\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {x}\to {\phi }\right)\right)↔\left({B}\in \mathrm{\omega }\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
27 sseq2 ${⊢}{x}={A}\to \left({B}\subseteq {x}↔{B}\subseteq {A}\right)$
28 27 4 imbi12d ${⊢}{x}={A}\to \left(\left({B}\subseteq {x}\to {\phi }\right)↔\left({B}\subseteq {A}\to {\tau }\right)\right)$
29 28 imbi2d ${⊢}{x}={A}\to \left(\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {x}\to {\phi }\right)\right)↔\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {A}\to {\tau }\right)\right)\right)$
30 5 a1d ${⊢}{B}\in \mathrm{\omega }\to \left({B}\subseteq \varnothing \to {\psi }\right)$
31 vex ${⊢}{y}\in \mathrm{V}$
32 31 sucex ${⊢}\mathrm{suc}{y}\in \mathrm{V}$
33 32 eqvinc ${⊢}\mathrm{suc}{y}={B}↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{suc}{y}\wedge {x}={B}\right)$
34 5 1 syl5ibr ${⊢}{x}={B}\to \left({B}\in \mathrm{\omega }\to {\phi }\right)$
35 3 biimpd ${⊢}{x}=\mathrm{suc}{y}\to \left({\phi }\to {\theta }\right)$
36 34 35 sylan9r ${⊢}\left({x}=\mathrm{suc}{y}\wedge {x}={B}\right)\to \left({B}\in \mathrm{\omega }\to {\theta }\right)$
37 36 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{suc}{y}\wedge {x}={B}\right)\to \left({B}\in \mathrm{\omega }\to {\theta }\right)$
38 33 37 sylbi ${⊢}\mathrm{suc}{y}={B}\to \left({B}\in \mathrm{\omega }\to {\theta }\right)$
39 38 eqcoms ${⊢}{B}=\mathrm{suc}{y}\to \left({B}\in \mathrm{\omega }\to {\theta }\right)$
40 39 imim2i ${⊢}\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)\to \left({B}\subseteq \mathrm{suc}{y}\to \left({B}\in \mathrm{\omega }\to {\theta }\right)\right)$
41 40 a1d ${⊢}\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to \left({B}\in \mathrm{\omega }\to {\theta }\right)\right)\right)$
42 41 com4r ${⊢}{B}\in \mathrm{\omega }\to \left(\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
43 42 adantl ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left(\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
44 df-ne ${⊢}{B}\ne \mathrm{suc}{y}↔¬{B}=\mathrm{suc}{y}$
45 44 anbi2i ${⊢}\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)↔\left({B}\subseteq \mathrm{suc}{y}\wedge ¬{B}=\mathrm{suc}{y}\right)$
46 annim ${⊢}\left({B}\subseteq \mathrm{suc}{y}\wedge ¬{B}=\mathrm{suc}{y}\right)↔¬\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)$
47 45 46 bitri ${⊢}\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)↔¬\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)$
48 nnon ${⊢}{B}\in \mathrm{\omega }\to {B}\in \mathrm{On}$
49 nnon ${⊢}{y}\in \mathrm{\omega }\to {y}\in \mathrm{On}$
50 onsssuc ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({B}\subseteq {y}↔{B}\in \mathrm{suc}{y}\right)$
51 suceloni ${⊢}{y}\in \mathrm{On}\to \mathrm{suc}{y}\in \mathrm{On}$
52 onelpss ${⊢}\left({B}\in \mathrm{On}\wedge \mathrm{suc}{y}\in \mathrm{On}\right)\to \left({B}\in \mathrm{suc}{y}↔\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)\right)$
53 51 52 sylan2 ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({B}\in \mathrm{suc}{y}↔\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)\right)$
54 50 53 bitrd ${⊢}\left({B}\in \mathrm{On}\wedge {y}\in \mathrm{On}\right)\to \left({B}\subseteq {y}↔\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)\right)$
55 48 49 54 syl2anr ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left({B}\subseteq {y}↔\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)\right)$
56 6 ex ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left({B}\subseteq {y}\to \left({\chi }\to {\theta }\right)\right)$
57 56 a1ddd ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left({B}\subseteq {y}\to \left({\chi }\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
58 57 a2d ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq {y}\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
59 58 com23 ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left({B}\subseteq {y}\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
60 55 59 sylbird ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left(\left({B}\subseteq \mathrm{suc}{y}\wedge {B}\ne \mathrm{suc}{y}\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
61 47 60 syl5bir ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left(¬\left({B}\subseteq \mathrm{suc}{y}\to {B}=\mathrm{suc}{y}\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
62 43 61 pm2.61d ${⊢}\left({y}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)$
63 62 ex ${⊢}{y}\in \mathrm{\omega }\to \left({B}\in \mathrm{\omega }\to \left(\left({B}\subseteq {y}\to {\chi }\right)\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
64 63 a2d ${⊢}{y}\in \mathrm{\omega }\to \left(\left({B}\in \mathrm{\omega }\to \left({B}\subseteq {y}\to {\chi }\right)\right)\to \left({B}\in \mathrm{\omega }\to \left({B}\subseteq \mathrm{suc}{y}\to {\theta }\right)\right)\right)$
65 20 23 26 29 30 64 finds ${⊢}{A}\in \mathrm{\omega }\to \left({B}\in \mathrm{\omega }\to \left({B}\subseteq {A}\to {\tau }\right)\right)$
66 65 imp31 ${⊢}\left(\left({A}\in \mathrm{\omega }\wedge {B}\in \mathrm{\omega }\right)\wedge {B}\subseteq {A}\right)\to {\tau }$