Theorem axrepprim

Description: ax-rep without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010)

	Ref	Expression
Assertion	axrepprim	$$⊢\neg \forall x\neg \left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		axrepnd	$$⊢\exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\right)$$
2		df-ex	$$⊢\exists y\forall z\left(\phi \to z=y\right)\leftrightarrow \neg \forall y\neg \forall z\left(\phi \to z=y\right)$$
3		df-an	$$⊢\left(\forall zx\in y\wedge \forall y\phi \right)\leftrightarrow \neg \left(\forall zx\in y\to \neg \forall y\phi \right)$$
4	3	exbii	$$⊢\exists x\left(\forall zx\in y\wedge \forall y\phi \right)\leftrightarrow \exists x\neg \left(\forall zx\in y\to \neg \forall y\phi \right)$$
5		exnal	$$⊢\exists x\neg \left(\forall zx\in y\to \neg \forall y\phi \right)\leftrightarrow \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)$$
6	4 5	bitri	$$⊢\exists x\left(\forall zx\in y\wedge \forall y\phi \right)\leftrightarrow \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)$$
7	6	bibi2i	$$⊢\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\leftrightarrow \left(\forall yz\in x\leftrightarrow \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)$$
8		dfbi1	$$⊢\left(\forall yz\in x\leftrightarrow \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\leftrightarrow \neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)$$
9	7 8	bitri	$$⊢\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\leftrightarrow \neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)$$
10	9	albii	$$⊢\forall z\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\leftrightarrow \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)$$
11	2 10	imbi12i	$$⊢\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\right)\leftrightarrow \left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)$$
12	11	exbii	$$⊢\exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\right)\leftrightarrow \exists x\left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)$$
13		df-ex	$$⊢\exists x\left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)\leftrightarrow \neg \forall x\neg \left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)$$
14	12 13	bitri	$$⊢\exists x\left(\exists y\forall z\left(\phi \to z=y\right)\to \forall z\left(\forall yz\in x\leftrightarrow \exists x\left(\forall zx\in y\wedge \forall y\phi \right)\right)\right)\leftrightarrow \neg \forall x\neg \left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)$$
15	1 14	mpbi	$$⊢\neg \forall x\neg \left(\neg \forall y\neg \forall z\left(\phi \to z=y\right)\to \forall z\neg \left(\left(\forall yz\in x\to \neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\right)\to \neg \left(\neg \forall x\left(\forall zx\in y\to \neg \forall y\phi \right)\to \forall yz\in x\right)\right)\right)$$