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