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