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