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 9511
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 9512 shows it converted to abbreviations. This axiom was derived as Theorem axinf2 9510 above, using our version of Infinity ax-inf 9508 and the Axiom of Regularity ax-reg 9462. We will reference ax-inf2 9511 instead of axinf2 9510 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 9508 from ax-inf2 9511 is shown by Theorem axinf 9514. (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 2108 . . . . 5 wff 𝑦𝑥
4 vz . . . . . . . 8 setvar 𝑧
54, 1wel 2108 . . . . . . 7 wff 𝑧𝑦
65wn 3 . . . . . 6 wff ¬ 𝑧𝑦
76, 4wal 1540 . . . . 5 wff 𝑧 ¬ 𝑧𝑦
83, 7wa 397 . . . 4 wff (𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦)
98, 1wex 1782 . . 3 wff 𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦)
104, 2wel 2108 . . . . . . 7 wff 𝑧𝑥
11 vw . . . . . . . . . 10 setvar 𝑤
1211, 4wel 2108 . . . . . . . . 9 wff 𝑤𝑧
1311, 1wel 2108 . . . . . . . . . 10 wff 𝑤𝑦
1411, 1weq 1967 . . . . . . . . . 10 wff 𝑤 = 𝑦
1513, 14wo 846 . . . . . . . . 9 wff (𝑤𝑦𝑤 = 𝑦)
1612, 15wb 205 . . . . . . . 8 wff (𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))
1716, 11wal 1540 . . . . . . 7 wff 𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))
1810, 17wa 397 . . . . . 6 wff (𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))
1918, 4wex 1782 . . . . 5 wff 𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))
203, 19wi 4 . . . 4 wff (𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))))
2120, 1wal 1540 . . 3 wff 𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦))))
229, 21wa 397 . 2 wff (∃𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) ∧ ∀𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))))
2322, 2wex 1782 1 wff 𝑥(∃𝑦(𝑦𝑥 ∧ ∀𝑧 ¬ 𝑧𝑦) ∧ ∀𝑦(𝑦𝑥 → ∃𝑧(𝑧𝑥 ∧ ∀𝑤(𝑤𝑧 ↔ (𝑤𝑦𝑤 = 𝑦)))))
Colors of variables: wff setvar class
This axiom is referenced by:  zfinf2  9512
  Copyright terms: Public domain W3C validator