Metamath Proof Explorer

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 ⊢ ∃ x ∅ ∈ x ∧ ∀ y ∈ x y ∈ x ↔ ¬ ∀ x ¬ ∀ y ∀ z ∀ w w ∈ y → ¬ w ∈ x → ¬ w = z → y ∈ x

Proof

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