Theorem nmo

Description: Negation of "at most one". (Contributed by Thierry Arnoux, 26-Feb-2017)

	Ref	Expression
Hypothesis	nmo.1	$$⊢Ⅎy\phi$$
Assertion	nmo	$$⊢\neg {\exists }^{*}x\phi \leftrightarrow \forall y\exists x\left(\phi \wedge x\ne y\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmo.1	$$⊢Ⅎy\phi$$
2	1	mof	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$
3	2	notbii	$$⊢\neg {\exists }^{*}x\phi \leftrightarrow \neg \exists y\forall x\left(\phi \to x=y\right)$$
4		alnex	$$⊢\forall y\neg \forall x\left(\phi \to x=y\right)\leftrightarrow \neg \exists y\forall x\left(\phi \to x=y\right)$$
5		exnal	$$⊢\exists x\neg \left(\phi \to x=y\right)\leftrightarrow \neg \forall x\left(\phi \to x=y\right)$$
6		pm4.61	$$⊢\neg \left(\phi \to x=y\right)\leftrightarrow \left(\phi \wedge \neg x=y\right)$$
7		biid	$$⊢x=y\leftrightarrow x=y$$
8	7	necon3bbii	$$⊢\neg x=y\leftrightarrow x\ne y$$
9	8	anbi2i	$$⊢\left(\phi \wedge \neg x=y\right)\leftrightarrow \left(\phi \wedge x\ne y\right)$$
10	6 9	bitri	$$⊢\neg \left(\phi \to x=y\right)\leftrightarrow \left(\phi \wedge x\ne y\right)$$
11	10	exbii	$$⊢\exists x\neg \left(\phi \to x=y\right)\leftrightarrow \exists x\left(\phi \wedge x\ne y\right)$$
12	5 11	bitr3i	$$⊢\neg \forall x\left(\phi \to x=y\right)\leftrightarrow \exists x\left(\phi \wedge x\ne y\right)$$
13	12	albii	$$⊢\forall y\neg \forall x\left(\phi \to x=y\right)\leftrightarrow \forall y\exists x\left(\phi \wedge x\ne y\right)$$
14	3 4 13	3bitr2i	$$⊢\neg {\exists }^{*}x\phi \leftrightarrow \forall y\exists x\left(\phi \wedge x\ne y\right)$$