Theorem ax12inda

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Quantification case. (When z and y are distinct, ax12inda2 may be used instead to avoid the dummy variable w in the proof.) (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ax12inda.1	$$⊢\neg \forall xx=w\to \left(x=w\to \left(\phi \to \forall x\left(x=w\to \phi \right)\right)\right)$$
Assertion	ax12inda	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax12inda.1	$$⊢\neg \forall xx=w\to \left(x=w\to \left(\phi \to \forall x\left(x=w\to \phi \right)\right)\right)$$
2		ax6ev	$$⊢\exists ww=y$$
3	1	ax12inda2	$$⊢\neg \forall xx=w\to \left(x=w\to \left(\forall z\phi \to \forall x\left(x=w\to \forall z\phi \right)\right)\right)$$
4		dveeq2-o	$$⊢\neg \forall xx=y\to \left(w=y\to \forall xw=y\right)$$
5	4	imp	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \forall xw=y$$
6		hba1-o	$$⊢\forall xw=y\to \forall x\forall xw=y$$
7		equequ2	$$⊢w=y\to \left(x=w\leftrightarrow x=y\right)$$
8	7	sps-o	$$⊢\forall xw=y\to \left(x=w\leftrightarrow x=y\right)$$
9	6 8	albidh	$$⊢\forall xw=y\to \left(\forall xx=w\leftrightarrow \forall xx=y\right)$$
10	9	notbid	$$⊢\forall xw=y\to \left(\neg \forall xx=w\leftrightarrow \neg \forall xx=y\right)$$
11	5 10	syl	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\neg \forall xx=w\leftrightarrow \neg \forall xx=y\right)$$
12	7	adantl	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(x=w\leftrightarrow x=y\right)$$
13	8	imbi1d	$$⊢\forall xw=y\to \left(\left(x=w\to \forall z\phi \right)\leftrightarrow \left(x=y\to \forall z\phi \right)\right)$$
14	6 13	albidh	$$⊢\forall xw=y\to \left(\forall x\left(x=w\to \forall z\phi \right)\leftrightarrow \forall x\left(x=y\to \forall z\phi \right)\right)$$
15	5 14	syl	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\forall x\left(x=w\to \forall z\phi \right)\leftrightarrow \forall x\left(x=y\to \forall z\phi \right)\right)$$
16	15	imbi2d	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\left(\forall z\phi \to \forall x\left(x=w\to \forall z\phi \right)\right)\leftrightarrow \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$
17	12 16	imbi12d	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\left(x=w\to \left(\forall z\phi \to \forall x\left(x=w\to \forall z\phi \right)\right)\right)\leftrightarrow \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)$$
18	11 17	imbi12d	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\left(\neg \forall xx=w\to \left(x=w\to \left(\forall z\phi \to \forall x\left(x=w\to \forall z\phi \right)\right)\right)\right)\leftrightarrow \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)\right)$$
19	3 18	mpbii	$$⊢\left(\neg \forall xx=y\wedge w=y\right)\to \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)$$
20	19	ex	$$⊢\neg \forall xx=y\to \left(w=y\to \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)\right)$$
21	20	exlimdv	$$⊢\neg \forall xx=y\to \left(\exists ww=y\to \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)\right)$$
22	2 21	mpi	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)\right)$$
23	22	pm2.43i	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$