Theorem tfinds2

Description: Transfinite Induction (inference schema), using implicit substitutions. The first three hypotheses establish the substitutions we need. The last three are the basis and the induction hypotheses (for successor and limit ordinals respectively). Theorem Schema 4 of Suppes p. 197. The wff ta is an auxiliary antecedent to help shorten proofs using this theorem. (Contributed by NM, 4-Sep-2004)

	Ref	Expression
Hypotheses	tfinds2.1	$$⊢x=\varnothing \to \left(\phi \leftrightarrow \psi \right)$$
	tfinds2.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	tfinds2.3	$$⊢x=\mathrm{suc}y\to \left(\phi \leftrightarrow \theta \right)$$
	tfinds2.4	$$⊢\tau \to \psi$$
	tfinds2.5	$$⊢y\in \mathrm{On}\to \left(\tau \to \left(\chi \to \theta \right)\right)$$
	tfinds2.6	$$⊢\mathrm{Lim}x\to \left(\tau \to \left(\forall y\in x\chi \to \phi \right)\right)$$
Assertion	tfinds2	$$⊢x\in \mathrm{On}\to \left(\tau \to \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		tfinds2.1	$$⊢x=\varnothing \to \left(\phi \leftrightarrow \psi \right)$$
2		tfinds2.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
3		tfinds2.3	$$⊢x=\mathrm{suc}y\to \left(\phi \leftrightarrow \theta \right)$$
4		tfinds2.4	$$⊢\tau \to \psi$$
5		tfinds2.5	$$⊢y\in \mathrm{On}\to \left(\tau \to \left(\chi \to \theta \right)\right)$$
6		tfinds2.6	$$⊢\mathrm{Lim}x\to \left(\tau \to \left(\forall y\in x\chi \to \phi \right)\right)$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8	1	imbi2d	$$⊢x=\varnothing \to \left(\left(\tau \to \phi \right)\leftrightarrow \left(\tau \to \psi \right)\right)$$
9	7 8	sbcie	$$⊢\underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}\left(\tau \to \phi \right)\leftrightarrow \left(\tau \to \psi \right)$$
10	4 9	mpbir	$$⊢\underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}\left(\tau \to \phi \right)$$
11	5	a2d	$$⊢y\in \mathrm{On}\to \left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)$$
12	11	sbcth	$$⊢x\in \mathrm{V}\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(y\in \mathrm{On}\to \left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\right)$$
13	12	elv	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(y\in \mathrm{On}\to \left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\right)$$
14		sbcimg	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(y\in \mathrm{On}\to \left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}y\in \mathrm{On}\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\right)\right)$$
15	14	elv	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(y\in \mathrm{On}\to \left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}y\in \mathrm{On}\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\right)$$
16	13 15	mpbi	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}y\in \mathrm{On}\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)$$
17		sbcel1v	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}y\in \mathrm{On}\leftrightarrow x\in \mathrm{On}$$
18		sbcimg	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \chi \right)\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \theta \right)\right)\right)$$
19	18	elv	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\left(\tau \to \chi \right)\to \left(\tau \to \theta \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \chi \right)\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \theta \right)\right)$$
20	16 17 19	3imtr3i	$$⊢x\in \mathrm{On}\to \left(\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \chi \right)\to \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \theta \right)\right)$$
21		vex	$$⊢x\in \mathrm{V}$$
22	2	bicomd	$$⊢x=y\to \left(\chi \leftrightarrow \phi \right)$$
23	22	equcoms	$$⊢y=x\to \left(\chi \leftrightarrow \phi \right)$$
24	23	imbi2d	$$⊢y=x\to \left(\left(\tau \to \chi \right)\leftrightarrow \left(\tau \to \phi \right)\right)$$
25	21 24	sbcie	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \chi \right)\leftrightarrow \left(\tau \to \phi \right)$$
26		vex	$$⊢y\in \mathrm{V}$$
27	26	sucex	$$⊢\mathrm{suc}y\in \mathrm{V}$$
28	3	imbi2d	$$⊢x=\mathrm{suc}y\to \left(\left(\tau \to \phi \right)\leftrightarrow \left(\tau \to \theta \right)\right)$$
29	27 28	sbcie	$$⊢\underset{\dot{}}{[}\mathrm{suc}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\leftrightarrow \left(\tau \to \theta \right)$$
30	29	sbcbii	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{suc}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\leftrightarrow \underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \theta \right)$$
31		suceq	$$⊢x=y\to \mathrm{suc}x=\mathrm{suc}y$$
32	31	sbcco2	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{suc}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\leftrightarrow \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\left(\tau \to \phi \right)$$
33	30 32	bitr3i	$$⊢\underset{\dot{}}{[}x/y\underset{\dot{}}{]}\left(\tau \to \theta \right)\leftrightarrow \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\left(\tau \to \phi \right)$$
34	20 25 33	3imtr3g	$$⊢x\in \mathrm{On}\to \left(\left(\tau \to \phi \right)\to \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\right)$$
35	2	imbi2d	$$⊢x=y\to \left(\left(\tau \to \phi \right)\leftrightarrow \left(\tau \to \chi \right)\right)$$
36	35	sbralie	$$⊢\forall x\in y\left(\tau \to \phi \right)\leftrightarrow \left[y/x\right]\forall y\in x\left(\tau \to \chi \right)$$
37		sbsbc	$$⊢\left[y/x\right]\forall y\in x\left(\tau \to \chi \right)\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\forall y\in x\left(\tau \to \chi \right)$$
38	36 37	bitr2i	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\forall y\in x\left(\tau \to \chi \right)\leftrightarrow \forall x\in y\left(\tau \to \phi \right)$$
39		r19.21v	$$⊢\forall y\in x\left(\tau \to \chi \right)\leftrightarrow \left(\tau \to \forall y\in x\chi \right)$$
40	6	a2d	$$⊢\mathrm{Lim}x\to \left(\left(\tau \to \forall y\in x\chi \right)\to \left(\tau \to \phi \right)\right)$$
41	39 40	syl5bi	$$⊢\mathrm{Lim}x\to \left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)$$
42	41	sbcth	$$⊢y\in \mathrm{V}\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\mathrm{Lim}x\to \left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\right)$$
43	42	elv	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\mathrm{Lim}x\to \left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\right)$$
44		sbcimg	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\mathrm{Lim}x\to \left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\mathrm{Lim}x\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\right)\right)$$
45	44	elv	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\mathrm{Lim}x\to \left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\mathrm{Lim}x\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\right)$$
46	43 45	mpbi	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\mathrm{Lim}x\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)$$
47		limeq	$$⊢x=y\to \left(\mathrm{Lim}x\leftrightarrow \mathrm{Lim}y\right)$$
48	26 47	sbcie	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\mathrm{Lim}x\leftrightarrow \mathrm{Lim}y$$
49		sbcimg	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\forall y\in x\left(\tau \to \chi \right)\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\right)\right)$$
50	49	elv	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\forall y\in x\left(\tau \to \chi \right)\to \left(\tau \to \phi \right)\right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\forall y\in x\left(\tau \to \chi \right)\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\right)$$
51	46 48 50	3imtr3i	$$⊢\mathrm{Lim}y\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\forall y\in x\left(\tau \to \chi \right)\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\right)$$
52	38 51	syl5bir	$$⊢\mathrm{Lim}y\to \left(\forall x\in y\left(\tau \to \phi \right)\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\left(\tau \to \phi \right)\right)$$
53	10 34 52	tfindes	$$⊢x\in \mathrm{On}\to \left(\tau \to \phi \right)$$