Theorem ax12inda2ALT

Description: Alternate proof of ax12inda2 , slightly more direct and not requiring ax-c16 . (Contributed by NM, 4-May-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ax12inda2.1	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
Assertion	ax12inda2ALT	$$⊢\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		ax12inda2.1	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
2		ax-1	$$⊢\forall x\phi \to \left(x=y\to \forall x\phi \right)$$
3	2	axc4i-o	$$⊢\forall x\phi \to \forall x\left(x=y\to \forall x\phi \right)$$
4	3	a1i	$$⊢\forall zz=x\to \left(\forall x\phi \to \forall x\left(x=y\to \forall x\phi \right)\right)$$
5		biidd	$$⊢\forall zz=x\to \left(\phi \leftrightarrow \phi \right)$$
6	5	dral1-o	$$⊢\forall zz=x\to \left(\forall z\phi \leftrightarrow \forall x\phi \right)$$
7	6	imbi2d	$$⊢\forall zz=x\to \left(\left(x=y\to \forall z\phi \right)\leftrightarrow \left(x=y\to \forall x\phi \right)\right)$$
8	7	dral2-o	$$⊢\forall zz=x\to \left(\forall x\left(x=y\to \forall z\phi \right)\leftrightarrow \forall x\left(x=y\to \forall x\phi \right)\right)$$
9	4 6 8	3imtr4d	$$⊢\forall zz=x\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)$$
10	9	aecoms-o	$$⊢\forall xx=z\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)$$
11	10	a1d	$$⊢\forall xx=z\to \left(x=y\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)\right)$$
12	11	a1d	$$⊢\forall xx=z\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)$$
13		simplr	$$⊢\left(\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \neg \forall xx=y$$
14		dveeq1-o	$$⊢\neg \forall zz=x\to \left(x=y\to \forall zx=y\right)$$
15	14	naecoms-o	$$⊢\neg \forall xx=z\to \left(x=y\to \forall zx=y\right)$$
16	15	imp	$$⊢\left(\neg \forall xx=z\wedge x=y\right)\to \forall zx=y$$
17	16	adantlr	$$⊢\left(\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \forall zx=y$$
18		hbnae-o	$$⊢\neg \forall xx=y\to \forall z\neg \forall xx=y$$
19		hba1-o	$$⊢\forall zx=y\to \forall z\forall zx=y$$
20	18 19	hban	$$⊢\left(\neg \forall xx=y\wedge \forall zx=y\right)\to \forall z\left(\neg \forall xx=y\wedge \forall zx=y\right)$$
21		ax-c5	$$⊢\forall zx=y\to x=y$$
22	1	imp	$$⊢\left(\neg \forall xx=y\wedge x=y\right)\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
23	21 22	sylan2	$$⊢\left(\neg \forall xx=y\wedge \forall zx=y\right)\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
24	20 23	alimdh	$$⊢\left(\neg \forall xx=y\wedge \forall zx=y\right)\to \left(\forall z\phi \to \forall z\forall x\left(x=y\to \phi \right)\right)$$
25	13 17 24	syl2anc	$$⊢\left(\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \left(\forall z\phi \to \forall z\forall x\left(x=y\to \phi \right)\right)$$
26		ax-11	$$⊢\forall z\forall x\left(x=y\to \phi \right)\to \forall x\forall z\left(x=y\to \phi \right)$$
27		hbnae-o	$$⊢\neg \forall xx=z\to \forall x\neg \forall xx=z$$
28		hbnae-o	$$⊢\neg \forall xx=z\to \forall z\neg \forall xx=z$$
29	28 15	nf5dh	$$⊢\neg \forall xx=z\to Ⅎzx=y$$
30		19.21t	$$⊢Ⅎzx=y\to \left(\forall z\left(x=y\to \phi \right)\leftrightarrow \left(x=y\to \forall z\phi \right)\right)$$
31	29 30	syl	$$⊢\neg \forall xx=z\to \left(\forall z\left(x=y\to \phi \right)\leftrightarrow \left(x=y\to \forall z\phi \right)\right)$$
32	27 31	albidh	$$⊢\neg \forall xx=z\to \left(\forall x\forall z\left(x=y\to \phi \right)\leftrightarrow \forall x\left(x=y\to \forall z\phi \right)\right)$$
33	26 32	syl5ib	$$⊢\neg \forall xx=z\to \left(\forall z\forall x\left(x=y\to \phi \right)\to \forall x\left(x=y\to \forall z\phi \right)\right)$$
34	33	ad2antrr	$$⊢\left(\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \left(\forall z\forall x\left(x=y\to \phi \right)\to \forall x\left(x=y\to \forall z\phi \right)\right)$$
35	25 34	syld	$$⊢\left(\left(\neg \forall xx=z\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \left(\forall z\phi \to \forall x\left(x=y\to \forall z\phi \right)\right)$$
36	35	exp31	$$⊢\neg \forall xx=z\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)$$
37	12 36	pm2.61i	$$⊢\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)$$