MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-inf2 Structured version   Visualization version   GIF version

Axiom ax-inf2 8231
Description: A standard version of Axiom of Infinity of ZF set theory. In English, it says: there exists a set that contains the empty set and the successors of all of its members. Theorem zfinf2 8232 shows it converted to abbreviations. This axiom was derived as theorem axinf2 8230 above, using our version of Infinity ax-inf 8228 and the Axiom of Regularity ax-reg 8190. We will reference ax-inf2 8231 instead of axinf2 8230 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 8228 from ax-inf2 8231 is shown by theorem axinf 8234. (Contributed by NM, 3-Nov-1996.)
Assertion
Ref Expression
ax-inf2 𝑥(∃𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) ∧ ∀𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤

Detailed syntax breakdown of Axiom ax-inf2
StepHypRef Expression
1 vy . . . . . 6 setvar 𝑦
2 vx . . . . . 6 setvar 𝑥
31, 2wel 1938 . . . . 5 wff 𝑦𝑥
4 vz . . . . . . . 8 setvar 𝑧
54, 1wel 1938 . . . . . . 7 wff 𝑧𝑦
65wn 3 . . . . . 6 wff ¬ 𝑧𝑦
76, 4wal 1466 . . . . 5 wff 𝑧 ¬ 𝑧𝑦
83, 7wa 378 . . . 4 wff (𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦)
98, 1wex 1692 . . 3 wff 𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦)
104, 2wel 1938 . . . . . . 7 wff 𝑧𝑥
11 vw . . . . . . . . . 10 setvar 𝑤
1211, 4wel 1938 . . . . . . . . 9 wff 𝑤𝑧
1311, 1wel 1938 . . . . . . . . . 10 wff 𝑤𝑦
1411, 1weq 1822 . . . . . . . . . 10 wff 𝑤 = 𝑦
1513, 14wo 377 . . . . . . . . 9 wff (𝑤𝑦𝑤 = 𝑦)
1612, 15wb 191 . . . . . . . 8 wff (𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))
1716, 11wal 1466 . . . . . . 7 wff 𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))
1810, 17wa 378 . . . . . 6 wff (𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))
1918, 4wex 1692 . . . . 5 wff 𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))
203, 19wi 4 . . . 4 wff (𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))))
2120, 1wal 1466 . . 3 wff 𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))))
229, 21wa 378 . 2 wff (∃𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) ∧ ∀𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))))
2322, 2wex 1692 1 wff 𝑥(∃𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) ∧ ∀𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))))
Colors of variables: wff setvar class
This axiom is referenced by:  zfinf2  8232
  Copyright terms: Public domain W3C validator