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	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ) ↔ ¬ ∀ 𝑦 ¬ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑧 = 𝑥 → { 𝑧 } = { 𝑥 } )
2	1	eleq1d	⊢ ( 𝑧 = 𝑥 → ( { 𝑧 } ∈ 𝑦 ↔ { 𝑥 } ∈ 𝑦 ) )
3	2	cbvralvw	⊢ ( ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝑦 { 𝑥 } ∈ 𝑦 )
4		dfclel	⊢ ( { 𝑥 } ∈ 𝑦 ↔ ∃ 𝑧 ( 𝑧 = { 𝑥 } ∧ 𝑧 ∈ 𝑦 ) )
5		dfcleq	⊢ ( 𝑧 = { 𝑥 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑥 } ) )
6		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
7	6	bibi2i	⊢ ( ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝑧 ↔ 𝑦 = 𝑥 ) )
8		dfbi1	⊢ ( ( 𝑦 ∈ 𝑧 ↔ 𝑦 = 𝑥 ) ↔ ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) )
9	7 8	bitri	⊢ ( ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑥 } ) ↔ ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) )
10	9	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ { 𝑥 } ) ↔ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) )
11	5 10	bitri	⊢ ( 𝑧 = { 𝑥 } ↔ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) )
12	11	anbi2ci	⊢ ( ( 𝑧 = { 𝑥 } ∧ 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
13		df-an	⊢ ( ( 𝑧 ∈ 𝑦 ∧ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ↔ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
14	12 13	bitri	⊢ ( ( 𝑧 = { 𝑥 } ∧ 𝑧 ∈ 𝑦 ) ↔ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
15	14	exbii	⊢ ( ∃ 𝑧 ( 𝑧 = { 𝑥 } ∧ 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑧 ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
16		df-ex	⊢ ( ∃ 𝑧 ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ↔ ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
17	4 15 16	3bitri	⊢ ( { 𝑥 } ∈ 𝑦 ↔ ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
18	17	ralbii	⊢ ( ∀ 𝑥 ∈ 𝑦 { 𝑥 } ∈ 𝑦 ↔ ∀ 𝑥 ∈ 𝑦 ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
19		df-ral	⊢ ( ∀ 𝑥 ∈ 𝑦 ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) )
20	3 18 19	3bitri	⊢ ( ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) )
21	20	anbi2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )
22		df-an	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) ↔ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )
23	21 22	bitri	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ) ↔ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )
24	23	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ) ↔ ∃ 𝑦 ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )
25		df-ex	⊢ ( ∃ 𝑦 ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) ↔ ¬ ∀ 𝑦 ¬ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )
26	24 25	bitri	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 { 𝑧 } ∈ 𝑦 ) ↔ ¬ ∀ 𝑦 ¬ ¬ ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 ∈ 𝑦 → ¬ ∀ 𝑧 ¬ ¬ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑦 ¬ ( ( 𝑦 ∈ 𝑧 → 𝑦 = 𝑥 ) → ¬ ( 𝑦 = 𝑥 → 𝑦 ∈ 𝑧 ) ) ) ) ) )