Theorem mh-infprim3bi

Description: An axiom of infinity in primitive symbols not requiring ax-reg . This version of the axiom was designed by Stefan O'Rear for his zf2.nql program, see https://github.com/sorear/metamath-turing-machines . It directly implies ax-inf , but deriving ax-inf2 requires ax-ext and ax-rep , see mh-inf3sn . (Contributed by Matthew House, 13-Apr-2026)

	Ref	Expression
Assertion	mh-infprim3bi	$$⊢\exists y\left(x\in y\wedge \forall z\in y\left\{z\right\}\in y\right)\leftrightarrow \neg \forall y\neg \neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢z=x\to \left\{z\right\}=\left\{x\right\}$$
2	1	eleq1d	$$⊢z=x\to \left(\left\{z\right\}\in y\leftrightarrow \left\{x\right\}\in y\right)$$
3	2	cbvralvw	$$⊢\forall z\in y\left\{z\right\}\in y\leftrightarrow \forall x\in y\left\{x\right\}\in y$$
4		dfclel	$$⊢\left\{x\right\}\in y\leftrightarrow \exists z\left(z=\left\{x\right\}\wedge z\in y\right)$$
5		dfcleq	$$⊢z=\left\{x\right\}\leftrightarrow \forall y\left(y\in z\leftrightarrow y\in \left\{x\right\}\right)$$
6		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
7	6	bibi2i	$$⊢\left(y\in z\leftrightarrow y\in \left\{x\right\}\right)\leftrightarrow \left(y\in z\leftrightarrow y=x\right)$$
8		dfbi1	$$⊢\left(y\in z\leftrightarrow y=x\right)\leftrightarrow \neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)$$
9	7 8	bitri	$$⊢\left(y\in z\leftrightarrow y\in \left\{x\right\}\right)\leftrightarrow \neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)$$
10	9	albii	$$⊢\forall y\left(y\in z\leftrightarrow y\in \left\{x\right\}\right)\leftrightarrow \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)$$
11	5 10	bitri	$$⊢z=\left\{x\right\}\leftrightarrow \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)$$
12	11	anbi2ci	$$⊢\left(z=\left\{x\right\}\wedge z\in y\right)\leftrightarrow \left(z\in y\wedge \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
13		df-an	$$⊢\left(z\in y\wedge \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\leftrightarrow \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
14	12 13	bitri	$$⊢\left(z=\left\{x\right\}\wedge z\in y\right)\leftrightarrow \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
15	14	exbii	$$⊢\exists z\left(z=\left\{x\right\}\wedge z\in y\right)\leftrightarrow \exists z\neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
16		df-ex	$$⊢\exists z\neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\leftrightarrow \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
17	4 15 16	3bitri	$$⊢\left\{x\right\}\in y\leftrightarrow \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
18	17	ralbii	$$⊢\forall x\in y\left\{x\right\}\in y\leftrightarrow \forall x\in y\neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)$$
19		df-ral	$$⊢\forall x\in y\neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\leftrightarrow \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)$$
20	3 18 19	3bitri	$$⊢\forall z\in y\left\{z\right\}\in y\leftrightarrow \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)$$
21	20	anbi2i	$$⊢\left(x\in y\wedge \forall z\in y\left\{z\right\}\in y\right)\leftrightarrow \left(x\in y\wedge \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$
22		df-an	$$⊢\left(x\in y\wedge \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)\leftrightarrow \neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$
23	21 22	bitri	$$⊢\left(x\in y\wedge \forall z\in y\left\{z\right\}\in y\right)\leftrightarrow \neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$
24	23	exbii	$$⊢\exists y\left(x\in y\wedge \forall z\in y\left\{z\right\}\in y\right)\leftrightarrow \exists y\neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$
25		df-ex	$$⊢\exists y\neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)\leftrightarrow \neg \forall y\neg \neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$
26	24 25	bitri	$$⊢\exists y\left(x\in y\wedge \forall z\in y\left\{z\right\}\in y\right)\leftrightarrow \neg \forall y\neg \neg \left(x\in y\to \neg \forall x\left(x\in y\to \neg \forall z\neg \neg \left(z\in y\to \neg \forall y\neg \left(\left(y\in z\to y=x\right)\to \neg \left(y=x\to y\in z\right)\right)\right)\right)\right)$$