mh-infprim1bi

Description: Shortest possible axiom of infinity in primitive symbols. Deriving ax-inf or ax-inf2 from this axiom requires ax-ext , ax-rep , and ax-reg , see inf3 and inf0 . (Contributed by Matthew House, 13-Apr-2026)

		Ref	Expression
	Assertion	mh-infprim1bi	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow \neg \forall x \neg \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$

Proof

Step	Hyp	Ref	Expression
1		exnelv	$⊢ \exists y \neg y \in x$
2	1	a1bi	$⊢ x \neq \emptyset \leftrightarrow (\exists y \neg y \in x \to x \neq \emptyset)$
3		19.23v	$⊢ \forall y (\neg y \in x \to x \neq \emptyset) \leftrightarrow (\exists y \neg y \in x \to x \neq \emptyset)$
4		n0	$⊢ x \neq \emptyset \leftrightarrow \exists z z \in x$
5		pm2.21	$⊢ \neg y \in x \to (y \in x \to y \in z)$
6	5	biantrurd	$⊢ \neg y \in x \to (z \in x \leftrightarrow ((y \in x \to y \in z) \land z \in x))$
7	6	exbidv	$⊢ \neg y \in x \to (\exists z z \in x \leftrightarrow \exists z ((y \in x \to y \in z) \land z \in x))$
8	4 7	bitrid	$⊢ \neg y \in x \to (x \neq \emptyset \leftrightarrow \exists z ((y \in x \to y \in z) \land z \in x))$
9	8	pm5.74i	$⊢ (\neg y \in x \to x \neq \emptyset) \leftrightarrow (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))$
10	9	albii	$⊢ \forall y (\neg y \in x \to x \neq \emptyset) \leftrightarrow \forall y (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))$
11	2 3 10	3bitr2i	$⊢ x \neq \emptyset \leftrightarrow \forall y (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))$
12		df-ss	$⊢ x \subseteq ⋃ x \leftrightarrow \forall y (y \in x \to y \in ⋃ x)$
13		eluni	$⊢ y \in ⋃ x \leftrightarrow \exists z (y \in z \land z \in x)$
14		biimt	$⊢ y \in x \to (y \in z \leftrightarrow (y \in x \to y \in z))$
15	14	anbi1d	$⊢ y \in x \to ((y \in z \land z \in x) \leftrightarrow ((y \in x \to y \in z) \land z \in x))$
16	15	exbidv	$⊢ y \in x \to (\exists z (y \in z \land z \in x) \leftrightarrow \exists z ((y \in x \to y \in z) \land z \in x))$
17	13 16	bitrid	$⊢ y \in x \to (y \in ⋃ x \leftrightarrow \exists z ((y \in x \to y \in z) \land z \in x))$
18	17	pm5.74i	$⊢ (y \in x \to y \in ⋃ x) \leftrightarrow (y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))$
19	18	albii	$⊢ \forall y (y \in x \to y \in ⋃ x) \leftrightarrow \forall y (y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))$
20	12 19	bitri	$⊢ x \subseteq ⋃ x \leftrightarrow \forall y (y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))$
21	11 20	anbi12ci	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow (\forall y (y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)) \land \forall y (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)))$
22		19.26	$⊢ \forall y ((y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)) \land (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))) \leftrightarrow (\forall y (y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)) \land \forall y (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)))$
23		pm4.83	$⊢ ((y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)) \land (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))) \leftrightarrow \exists z ((y \in x \to y \in z) \land z \in x)$
24		exnalimn	$⊢ \exists z ((y \in x \to y \in z) \land z \in x) \leftrightarrow \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$
25	23 24	bitri	$⊢ ((y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)) \land (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))) \leftrightarrow \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$
26	25	albii	$⊢ \forall y ((y \in x \to \exists z ((y \in x \to y \in z) \land z \in x)) \land (\neg y \in x \to \exists z ((y \in x \to y \in z) \land z \in x))) \leftrightarrow \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$
27	21 22 26	3bitr2i	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$
28	27	exbii	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow \exists x \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$
29		df-ex	$⊢ \exists x \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x) \leftrightarrow \neg \forall x \neg \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$
30	28 29	bitri	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow \neg \forall x \neg \forall y \neg \forall z ((y \in x \to y \in z) \to \neg z \in x)$

Metamath Proof Explorer

Theorem mh-infprim1bi

Proof