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

Axiom ax-inf2 7358
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 7359 shows it converted to abbreviations. This axiom was derived as theorem axinf2 7357 above, using our version of Infinity ax-inf 7355 and the Axiom of Regularity ax-reg 7322. We will reference ax-inf2 7358 instead of axinf2 7357 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 7355 from ax-inf2 7358 is shown by theorem axinf 7361. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
ax-inf2  |-  E. x
( E. y ( y  e.  x  /\  A. z  -.  z  e.  y )  /\  A. y ( y  e.  x  ->  E. z
( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) ) )
Distinct variable group:    x, y, z, w

Detailed syntax breakdown of Axiom ax-inf2
StepHypRef Expression
1 vy . . . . . 6  set  y
2 vx . . . . . 6  set  x
31, 2wel 1697 . . . . 5  wff  y  e.  x
4 vz . . . . . . . 8  set  z
54, 1wel 1697 . . . . . . 7  wff  z  e.  y
65wn 3 . . . . . 6  wff  -.  z  e.  y
76, 4wal 1530 . . . . 5  wff  A. z  -.  z  e.  y
83, 7wa 358 . . . 4  wff  ( y  e.  x  /\  A. z  -.  z  e.  y )
98, 1wex 1531 . . 3  wff  E. y
( y  e.  x  /\  A. z  -.  z  e.  y )
104, 2wel 1697 . . . . . . 7  wff  z  e.  x
11 vw . . . . . . . . . 10  set  w
1211, 4wel 1697 . . . . . . . . 9  wff  w  e.  z
1311, 1wel 1697 . . . . . . . . . 10  wff  w  e.  y
1411, 1weq 1633 . . . . . . . . . 10  wff  w  =  y
1513, 14wo 357 . . . . . . . . 9  wff  ( w  e.  y  \/  w  =  y )
1612, 15wb 176 . . . . . . . 8  wff  ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) )
1716, 11wal 1530 . . . . . . 7  wff  A. w
( w  e.  z  <-> 
( w  e.  y  \/  w  =  y ) )
1810, 17wa 358 . . . . . 6  wff  ( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) )
1918, 4wex 1531 . . . . 5  wff  E. z
( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) )
203, 19wi 4 . . . 4  wff  ( y  e.  x  ->  E. z
( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) )
2120, 1wal 1530 . . 3  wff  A. y
( y  e.  x  ->  E. z ( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) )
229, 21wa 358 . 2  wff  ( E. y ( y  e.  x  /\  A. z  -.  z  e.  y
)  /\  A. y
( y  e.  x  ->  E. z ( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) ) )
2322, 2wex 1531 1  wff  E. x
( E. y ( y  e.  x  /\  A. z  -.  z  e.  y )  /\  A. y ( y  e.  x  ->  E. z
( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) ) )
Colors of variables: wff set class
This axiom is referenced by:  zfinf2  7359
  Copyright terms: Public domain W3C validator