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

Axiom ax-inf2 7625
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 7626 shows it converted to abbreviations. This axiom was derived as theorem axinf2 7624 above, using our version of Infinity ax-inf 7622 and the Axiom of Regularity ax-reg 7589. We will reference ax-inf2 7625 instead of axinf2 7624 so that the ordinary uses of Regularity can be more easily identified. The reverse derivation of ax-inf 7622 from ax-inf2 7625 is shown by theorem axinf 7628. (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 1728 . . . . 5  wff  y  e.  x
4 vz . . . . . . . 8  set  z
54, 1wel 1728 . . . . . . 7  wff  z  e.  y
65wn 3 . . . . . 6  wff  -.  z  e.  y
76, 4wal 1550 . . . . 5  wff  A. z  -.  z  e.  y
83, 7wa 360 . . . 4  wff  ( y  e.  x  /\  A. z  -.  z  e.  y )
98, 1wex 1551 . . 3  wff  E. y
( y  e.  x  /\  A. z  -.  z  e.  y )
104, 2wel 1728 . . . . . . 7  wff  z  e.  x
11 vw . . . . . . . . . 10  set  w
1211, 4wel 1728 . . . . . . . . 9  wff  w  e.  z
1311, 1wel 1728 . . . . . . . . . 10  wff  w  e.  y
1411, 1weq 1654 . . . . . . . . . 10  wff  w  =  y
1513, 14wo 359 . . . . . . . . 9  wff  ( w  e.  y  \/  w  =  y )
1612, 15wb 178 . . . . . . . 8  wff  ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) )
1716, 11wal 1550 . . . . . . 7  wff  A. w
( w  e.  z  <-> 
( w  e.  y  \/  w  =  y ) )
1810, 17wa 360 . . . . . 6  wff  ( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) )
1918, 4wex 1551 . . . . 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 1550 . . 3  wff  A. y
( y  e.  x  ->  E. z ( z  e.  x  /\  A. w ( w  e.  z  <->  ( w  e.  y  \/  w  =  y ) ) ) )
229, 21wa 360 . 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 1551 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  7626
  Copyright terms: Public domain W3C validator