Theorem ax12indalem

Description: Lemma for ax12inda2 and ax12inda . (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ax12indalem.1	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
Assertion	ax12indalem	$$⊢\neg \forall yy=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)$$

Proof

Step	Hyp	Ref	Expression
1		ax12indalem.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	12	adantr	$$⊢\left(\forall xx=z\wedge \neg \forall yy=z\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)$$
14		simplr	$$⊢\left(\left(\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \neg \forall xx=y$$
15		aecom-o	$$⊢\forall zz=x\to \forall xx=z$$
16	15	con3i	$$⊢\neg \forall xx=z\to \neg \forall zz=x$$
17		aecom-o	$$⊢\forall zz=y\to \forall yy=z$$
18	17	con3i	$$⊢\neg \forall yy=z\to \neg \forall zz=y$$
19		axc9	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x=y\to \forall zx=y\right)\right)$$
20	19	imp	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\to \forall zx=y\right)$$
21	16 18 20	syl2an	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\to \left(x=y\to \forall zx=y\right)$$
22	21	imp	$$⊢\left(\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\wedge x=y\right)\to \forall zx=y$$
23	22	adantlr	$$⊢\left(\left(\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\wedge \neg \forall xx=y\right)\wedge x=y\right)\to \forall zx=y$$
24		hbnae-o	$$⊢\neg \forall xx=y\to \forall z\neg \forall xx=y$$
25		hba1-o	$$⊢\forall zx=y\to \forall z\forall zx=y$$
26	24 25	hban	$$⊢\left(\neg \forall xx=y\wedge \forall zx=y\right)\to \forall z\left(\neg \forall xx=y\wedge \forall zx=y\right)$$
27		ax-c5	$$⊢\forall zx=y\to x=y$$
28	1	imp	$$⊢\left(\neg \forall xx=y\wedge x=y\right)\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
29	27 28	sylan2	$$⊢\left(\neg \forall xx=y\wedge \forall zx=y\right)\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)$$
30	26 29	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)$$
31	14 23 30	syl2anc	$$⊢\left(\left(\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\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)$$
32		ax-11	$$⊢\forall z\forall x\left(x=y\to \phi \right)\to \forall x\forall z\left(x=y\to \phi \right)$$
33		hbnae-o	$$⊢\neg \forall xx=z\to \forall x\neg \forall xx=z$$
34		hbnae-o	$$⊢\neg \forall yy=z\to \forall x\neg \forall yy=z$$
35	33 34	hban	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\to \forall x\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)$$
36		hbnae-o	$$⊢\neg \forall xx=z\to \forall z\neg \forall xx=z$$
37		hbnae-o	$$⊢\neg \forall yy=z\to \forall z\neg \forall yy=z$$
38	36 37	hban	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\to \forall z\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)$$
39	38 21	nf5dh	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\to Ⅎzx=y$$
40		19.21t	$$⊢Ⅎzx=y\to \left(\forall z\left(x=y\to \phi \right)\leftrightarrow \left(x=y\to \forall z\phi \right)\right)$$
41	39 40	syl	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\to \left(\forall z\left(x=y\to \phi \right)\leftrightarrow \left(x=y\to \forall z\phi \right)\right)$$
42	35 41	albidh	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\to \left(\forall x\forall z\left(x=y\to \phi \right)\leftrightarrow \forall x\left(x=y\to \forall z\phi \right)\right)$$
43	32 42	imbitrid	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\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)$$
44	43	ad2antrr	$$⊢\left(\left(\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\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)$$
45	31 44	syld	$$⊢\left(\left(\left(\neg \forall xx=z\wedge \neg \forall yy=z\right)\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)$$
46	45	exp31	$$⊢\left(\neg \forall xx=z\wedge \neg \forall yy=z\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)$$
47	13 46	pm2.61ian	$$⊢\neg \forall yy=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)$$