Theorem frinsg

Description: Well-Founded Induction Schema. If a property passes from all elements less than y of a well-founded class A to y itself (induction hypothesis), then the property holds for all elements of A . Theorem 5.6(ii) of Levy p. 64. (Contributed by Scott Fenton, 7-Feb-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypothesis	frinsg.1	$$⊢y\in A\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)$$
Assertion	frinsg	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to \forall y\in A\phi$$

Proof

Step	Hyp	Ref	Expression
1		frinsg.1	$$⊢y\in A\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)$$
2		ssrab2	$$⊢\left\{y\in A|\phi \right\}\subseteq A$$
3		dfss3	$$⊢Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\leftrightarrow \forall z\in Pred\left(R,A,w\right)z\in \left\{y\in A|\phi \right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
5	4	elrabsf	$$⊢z\in \left\{y\in A|\phi \right\}\leftrightarrow \left(z\in A\wedge \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right)$$
6	5	simprbi	$$⊢z\in \left\{y\in A|\phi \right\}\to \underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
7	6	ralimi	$$⊢\forall z\in Pred\left(R,A,w\right)z\in \left\{y\in A|\phi \right\}\to \forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
8	3 7	sylbi	$$⊢Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\to \forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
9		nfv	$$⊢Ⅎyw\in A$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yPred\left(R,A,w\right)$$
11		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
12	10 11	nfralw	$$⊢Ⅎy\forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
13		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi$$
14	12 13	nfim	$$⊢Ⅎy\left(\forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)$$
15	9 14	nfim	$$⊢Ⅎy\left(w\in A\to \left(\forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)\right)$$
16		eleq1w	$$⊢y=w\to \left(y\in A\leftrightarrow w\in A\right)$$
17		predeq3	$$⊢y=w\to Pred\left(R,A,y\right)=Pred\left(R,A,w\right)$$
18	17	raleqdv	$$⊢y=w\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right)$$
19		sbceq1a	$$⊢y=w\to \left(\phi \leftrightarrow \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)$$
20	18 19	imbi12d	$$⊢y=w\to \left(\left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)\leftrightarrow \left(\forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)\right)$$
21	16 20	imbi12d	$$⊢y=w\to \left(\left(y\in A\to \left(\forall z\in Pred\left(R,A,y\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \phi \right)\right)\leftrightarrow \left(w\in A\to \left(\forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)\right)\right)$$
22	15 21 1	chvarfv	$$⊢w\in A\to \left(\forall z\in Pred\left(R,A,w\right)\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)$$
23	8 22	syl5	$$⊢w\in A\to \left(Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\to \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)$$
24	23	anc2li	$$⊢w\in A\to \left(Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\to \left(w\in A\wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)\right)$$
25	4	elrabsf	$$⊢w\in \left\{y\in A|\phi \right\}\leftrightarrow \left(w\in A\wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)$$
26	24 25	syl6ibr	$$⊢w\in A\to \left(Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\to w\in \left\{y\in A|\phi \right\}\right)$$
27	26	rgen	$$⊢\forall w\in A\left(Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\to w\in \left\{y\in A|\phi \right\}\right)$$
28		frind	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\wedge \left(\left\{y\in A|\phi \right\}\subseteq A\wedge \forall w\in A\left(Pred\left(R,A,w\right)\subseteq \left\{y\in A|\phi \right\}\to w\in \left\{y\in A|\phi \right\}\right)\right)\right)\to A=\left\{y\in A|\phi \right\}$$
29	2 27 28	mpanr12	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to A=\left\{y\in A|\phi \right\}$$
30		rabid2	$$⊢A=\left\{y\in A|\phi \right\}\leftrightarrow \forall y\in A\phi$$
31	29 30	sylib	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to \forall y\in A\phi$$