Theorem mh-infprim2bi

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

	Ref	Expression
Assertion	mh-infprim2bi	⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
2	1	eleq1d	⊢ ( 𝑦 = 𝑧 → ( { 𝑦 } ∈ 𝑥 ↔ { 𝑧 } ∈ 𝑥 ) )
3	2	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ↔ ∀ 𝑧 ∈ 𝑥 { 𝑧 } ∈ 𝑥 )
4		df-ral	⊢ ( ∀ 𝑧 ∈ 𝑥 { 𝑧 } ∈ 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) )
5	3 4	bitri	⊢ ( ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) )
6	5	anbi2i	⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ) ↔ ( ∅ ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) )
7		pwin	⊢ 𝒫 ( { 𝑧 } ∩ 𝑥 ) = ( 𝒫 { 𝑧 } ∩ 𝒫 𝑥 )
8	7	raleqi	⊢ ( ∀ 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∈ ( 𝒫 { 𝑧 } ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑥 )
9		ralin	⊢ ( ∀ 𝑦 ∈ ( 𝒫 { 𝑧 } ∩ 𝒫 𝑥 ) 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝒫 { 𝑧 } ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) )
10		pwsn	⊢ 𝒫 { 𝑧 } = { ∅ , { 𝑧 } }
11	10	raleqi	⊢ ( ∀ 𝑦 ∈ 𝒫 { 𝑧 } ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ { ∅ , { 𝑧 } } ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) )
12	8 9 11	3bitrri	⊢ ( ∀ 𝑦 ∈ { ∅ , { 𝑧 } } ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) 𝑦 ∈ 𝑥 )
13		0ex	⊢ ∅ ∈ V
14		vsnex	⊢ { 𝑧 } ∈ V
15		eleq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ 𝒫 𝑥 ↔ ∅ ∈ 𝒫 𝑥 ) )
16		eleq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ 𝑥 ↔ ∅ ∈ 𝑥 ) )
17	15 16	imbi12d	⊢ ( 𝑦 = ∅ → ( ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ( ∅ ∈ 𝒫 𝑥 → ∅ ∈ 𝑥 ) ) )
18		0elpw	⊢ ∅ ∈ 𝒫 𝑥
19	18	a1bi	⊢ ( ∅ ∈ 𝑥 ↔ ( ∅ ∈ 𝒫 𝑥 → ∅ ∈ 𝑥 ) )
20	17 19	bitr4di	⊢ ( 𝑦 = ∅ → ( ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ∅ ∈ 𝑥 ) )
21		eleq1	⊢ ( 𝑦 = { 𝑧 } → ( 𝑦 ∈ 𝒫 𝑥 ↔ { 𝑧 } ∈ 𝒫 𝑥 ) )
22		vex	⊢ 𝑧 ∈ V
23	22	snelpw	⊢ ( 𝑧 ∈ 𝑥 ↔ { 𝑧 } ∈ 𝒫 𝑥 )
24	21 23	bitr4di	⊢ ( 𝑦 = { 𝑧 } → ( 𝑦 ∈ 𝒫 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
25		eleq1	⊢ ( 𝑦 = { 𝑧 } → ( 𝑦 ∈ 𝑥 ↔ { 𝑧 } ∈ 𝑥 ) )
26	24 25	imbi12d	⊢ ( 𝑦 = { 𝑧 } → ( ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) )
27	13 14 20 26	ralpr	⊢ ( ∀ 𝑦 ∈ { ∅ , { 𝑧 } } ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ( ∅ ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) )
28		df-ral	⊢ ( ∀ 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) 𝑦 ∈ 𝑥 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
29	12 27 28	3bitr3i	⊢ ( ( ∅ ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
30	29	albii	⊢ ( ∀ 𝑧 ( ∅ ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) ↔ ∀ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
31		19.28v	⊢ ( ∀ 𝑧 ( ∅ ∈ 𝑥 ∧ ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) ↔ ( ∅ ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) )
32		sneq	⊢ ( 𝑧 = 𝑤 → { 𝑧 } = { 𝑤 } )
33	32	ineq1d	⊢ ( 𝑧 = 𝑤 → ( { 𝑧 } ∩ 𝑥 ) = ( { 𝑤 } ∩ 𝑥 ) )
34	33	pweqd	⊢ ( 𝑧 = 𝑤 → 𝒫 ( { 𝑧 } ∩ 𝑥 ) = 𝒫 ( { 𝑤 } ∩ 𝑥 ) )
35	34	eleq2d	⊢ ( 𝑧 = 𝑤 → ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) ↔ 𝑦 ∈ 𝒫 ( { 𝑤 } ∩ 𝑥 ) ) )
36	35	imbi1d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝒫 ( { 𝑤 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) ) )
37		eleq1w	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) ↔ 𝑤 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) ) )
38		elequ1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
39	37 38	imbi12d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑤 ∈ 𝑥 ) ) )
40	36 39	alcomw	⊢ ( ∀ 𝑧 ∀ 𝑦 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
41	30 31 40	3bitr3i	⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → { 𝑧 } ∈ 𝑥 ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
42		velpw	⊢ ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) ↔ 𝑦 ⊆ ( { 𝑧 } ∩ 𝑥 ) )
43		df-ss	⊢ ( 𝑦 ⊆ ( { 𝑧 } ∩ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → 𝑤 ∈ ( { 𝑧 } ∩ 𝑥 ) ) )
44		elin	⊢ ( 𝑤 ∈ ( { 𝑧 } ∩ 𝑥 ) ↔ ( 𝑤 ∈ { 𝑧 } ∧ 𝑤 ∈ 𝑥 ) )
45		velsn	⊢ ( 𝑤 ∈ { 𝑧 } ↔ 𝑤 = 𝑧 )
46	45	anbi2ci	⊢ ( ( 𝑤 ∈ { 𝑧 } ∧ 𝑤 ∈ 𝑥 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑤 = 𝑧 ) )
47		df-an	⊢ ( ( 𝑤 ∈ 𝑥 ∧ 𝑤 = 𝑧 ) ↔ ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) )
48	44 46 47	3bitri	⊢ ( 𝑤 ∈ ( { 𝑧 } ∩ 𝑥 ) ↔ ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) )
49	48	imbi2i	⊢ ( ( 𝑤 ∈ 𝑦 → 𝑤 ∈ ( { 𝑧 } ∩ 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) )
50	49	albii	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → 𝑤 ∈ ( { 𝑧 } ∩ 𝑥 ) ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) )
51	42 43 50	3bitri	⊢ ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) )
52	51	imbi1i	⊢ ( ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) ↔ ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )
53	52	2albii	⊢ ( ∀ 𝑦 ∀ 𝑧 ( 𝑦 ∈ 𝒫 ( { 𝑧 } ∩ 𝑥 ) → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )
54	6 41 53	3bitri	⊢ ( ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ) ↔ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )
55	54	exbii	⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )
56		df-ex	⊢ ( ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )
57	55 56	bitri	⊢ ( ∃ 𝑥 ( ∅ ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 { 𝑦 } ∈ 𝑥 ) ↔ ¬ ∀ 𝑥 ¬ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑤 ( 𝑤 ∈ 𝑦 → ¬ ( 𝑤 ∈ 𝑥 → ¬ 𝑤 = 𝑧 ) ) → 𝑦 ∈ 𝑥 ) )