Theorem ax12indn

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Negation case. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax12indn.1	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\phi \to \forall x\left(x=y\to \phi \right)\right)\right)$$
2		19.8a	$$⊢\left(x=y\wedge \neg \phi \right)\to \exists x\left(x=y\wedge \neg \phi \right)$$
3		exanali	$$⊢\exists x\left(x=y\wedge \neg \phi \right)\leftrightarrow \neg \forall x\left(x=y\to \phi \right)$$
4		hbn1	$$⊢\neg \forall xx=y\to \forall x\neg \forall xx=y$$
5		hbn1	$$⊢\neg \forall x\left(x=y\to \phi \right)\to \forall x\neg \forall x\left(x=y\to \phi \right)$$
6		con3	$$⊢\left(\phi \to \forall x\left(x=y\to \phi \right)\right)\to \left(\neg \forall x\left(x=y\to \phi \right)\to \neg \phi \right)$$
7	1 6	syl6	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\neg \forall x\left(x=y\to \phi \right)\to \neg \phi \right)\right)$$
8	7	com23	$$⊢\neg \forall xx=y\to \left(\neg \forall x\left(x=y\to \phi \right)\to \left(x=y\to \neg \phi \right)\right)$$
9	4 5 8	alrimdh	$$⊢\neg \forall xx=y\to \left(\neg \forall x\left(x=y\to \phi \right)\to \forall x\left(x=y\to \neg \phi \right)\right)$$
10	3 9	biimtrid	$$⊢\neg \forall xx=y\to \left(\exists x\left(x=y\wedge \neg \phi \right)\to \forall x\left(x=y\to \neg \phi \right)\right)$$
11	2 10	syl5	$$⊢\neg \forall xx=y\to \left(\left(x=y\wedge \neg \phi \right)\to \forall x\left(x=y\to \neg \phi \right)\right)$$
12	11	expd	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\neg \phi \to \forall x\left(x=y\to \neg \phi \right)\right)\right)$$