Theorem 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	⊢ ( ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		exnelv	⊢ ∃ 𝑦 ¬ 𝑦 ∈ 𝑥
2	1	a1bi	⊢ ( 𝑥 ≠ ∅ ↔ ( ∃ 𝑦 ¬ 𝑦 ∈ 𝑥 → 𝑥 ≠ ∅ ) )
3		19.23v	⊢ ( ∀ 𝑦 ( ¬ 𝑦 ∈ 𝑥 → 𝑥 ≠ ∅ ) ↔ ( ∃ 𝑦 ¬ 𝑦 ∈ 𝑥 → 𝑥 ≠ ∅ ) )
4		n0	⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝑥 )
5		pm2.21	⊢ ( ¬ 𝑦 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
6	5	biantrurd	⊢ ( ¬ 𝑦 ∈ 𝑥 → ( 𝑧 ∈ 𝑥 ↔ ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
7	6	exbidv	⊢ ( ¬ 𝑦 ∈ 𝑥 → ( ∃ 𝑧 𝑧 ∈ 𝑥 ↔ ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
8	4 7	bitrid	⊢ ( ¬ 𝑦 ∈ 𝑥 → ( 𝑥 ≠ ∅ ↔ ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
9	8	pm5.74i	⊢ ( ( ¬ 𝑦 ∈ 𝑥 → 𝑥 ≠ ∅ ) ↔ ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
10	9	albii	⊢ ( ∀ 𝑦 ( ¬ 𝑦 ∈ 𝑥 → 𝑥 ≠ ∅ ) ↔ ∀ 𝑦 ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
11	2 3 10	3bitr2i	⊢ ( 𝑥 ≠ ∅ ↔ ∀ 𝑦 ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
12		df-ss	⊢ ( 𝑥 ⊆ ∪ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∪ 𝑥 ) )
13		eluni	⊢ ( 𝑦 ∈ ∪ 𝑥 ↔ ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) )
14		biimt	⊢ ( 𝑦 ∈ 𝑥 → ( 𝑦 ∈ 𝑧 ↔ ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) )
15	14	anbi1d	⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
16	15	exbidv	⊢ ( 𝑦 ∈ 𝑥 → ( ∃ 𝑧 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
17	13 16	bitrid	⊢ ( 𝑦 ∈ 𝑥 → ( 𝑦 ∈ ∪ 𝑥 ↔ ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
18	17	pm5.74i	⊢ ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∪ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
19	18	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∪ 𝑥 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
20	12 19	bitri	⊢ ( 𝑥 ⊆ ∪ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) )
21	11 20	anbi12ci	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ∧ ∀ 𝑦 ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ) )
22		19.26	⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ∧ ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ( ∀ 𝑦 ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ∧ ∀ 𝑦 ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ) )
23		pm4.83	⊢ ( ( ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ∧ ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) )
24		exnalimn	⊢ ( ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )
25	23 24	bitri	⊢ ( ( ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ∧ ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )
26	25	albii	⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ∧ ( ¬ 𝑦 ∈ 𝑥 → ∃ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )
27	21 22 26	3bitr2i	⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )
28	27	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )
29		df-ex	⊢ ( ∃ 𝑥 ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )
30	28 29	bitri	⊢ ( ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) → ¬ 𝑧 ∈ 𝑥 ) )