Theorem tfindes

Description: Transfinite Induction with explicit substitution. The first hypothesis is the basis, the second is the induction step for successors, and the third is the induction step for limit ordinals. Theorem Schema 4 of Suppes p. 197. (Contributed by NM, 5-Mar-2004)

	Ref	Expression
Hypotheses	tfindes.1	$$⊢\underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}\phi$$
	tfindes.2	$$⊢x\in \mathrm{On}\to \left(\phi \to \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\phi \right)$$
	tfindes.3	$$⊢\mathrm{Lim}y\to \left(\forall x\in y\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
Assertion	tfindes	$$⊢x\in \mathrm{On}\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		tfindes.1	$$⊢\underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}\phi$$
2		tfindes.2	$$⊢x\in \mathrm{On}\to \left(\phi \to \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\phi \right)$$
3		tfindes.3	$$⊢\mathrm{Lim}y\to \left(\forall x\in y\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
4		dfsbcq	$$⊢y=\varnothing \to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}\phi \right)$$
5		dfsbcq	$$⊢y=z\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
6		dfsbcq	$$⊢y=\mathrm{suc}z\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)$$
7		sbceq2a	$$⊢y=x\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
8		nfv	$$⊢Ⅎxz\in \mathrm{On}$$
9		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
10		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi$$
11	9 10	nfim	$$⊢Ⅎx\left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)$$
12	8 11	nfim	$$⊢Ⅎx\left(z\in \mathrm{On}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)\right)$$
13		eleq1w	$$⊢x=z\to \left(x\in \mathrm{On}\leftrightarrow z\in \mathrm{On}\right)$$
14		sbceq1a	$$⊢x=z\to \left(\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
15		suceq	$$⊢x=z\to \mathrm{suc}x=\mathrm{suc}z$$
16	15	sbceq1d	$$⊢x=z\to \left(\underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)$$
17	14 16	imbi12d	$$⊢x=z\to \left(\left(\phi \to \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)\right)$$
18	13 17	imbi12d	$$⊢x=z\to \left(\left(x\in \mathrm{On}\to \left(\phi \to \underset{\dot{}}{[}\mathrm{suc}x/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(z\in \mathrm{On}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
19	12 18 2	chvarfv	$$⊢z\in \mathrm{On}\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}\mathrm{suc}z/x\underset{\dot{}}{]}\phi \right)$$
20		cbvralsvw	$$⊢\forall x\in y\phi \leftrightarrow \forall z\in y\left[z/x\right]\phi$$
21		sbsbc	$$⊢\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
22	21	ralbii	$$⊢\forall z\in y\left[z/x\right]\phi \leftrightarrow \forall z\in y\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
23	20 22	bitri	$$⊢\forall x\in y\phi \leftrightarrow \forall z\in y\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
24	23 3	syl5bir	$$⊢\mathrm{Lim}y\to \left(\forall z\in y\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
25	4 5 6 7 1 19 24	tfinds	$$⊢x\in \mathrm{On}\to \phi$$