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

Theorem zfcndinf 8498
Description: Axiom of Infinity ax-inf 7596, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing theorem el 4384 in the proof. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by NM, 15-Aug-2003.)
Assertion
Ref Expression
zfcndinf  |-  E. y
( x  e.  y  /\  A. z ( z  e.  y  ->  E. w ( z  e.  w  /\  w  e.  y ) ) )
Distinct variable group:    x, y, z, w

Proof of Theorem zfcndinf
StepHypRef Expression
1 el 4384 . . 3  |-  E. w  x  e.  w
2 nfv 1630 . . . . . 6  |-  F/ w  x  e.  y
3 nfe1 1748 . . . . . . . 8  |-  F/ w E. w ( x  e.  w  /\  w  e.  y )
42, 3nfim 1833 . . . . . . 7  |-  F/ w
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) )
54nfal 1865 . . . . . 6  |-  F/ w A. x ( x  e.  y  ->  E. w
( x  e.  w  /\  w  e.  y
) )
62, 5nfan 1847 . . . . 5  |-  F/ w
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
76nfex 1866 . . . 4  |-  F/ w E. y ( x  e.  y  /\  A. x
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
8 axinfnd 8486 . . . . 5  |-  E. y
( x  e.  w  ->  ( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
9819.37aiv 1924 . . . 4  |-  ( x  e.  w  ->  E. y
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
107, 9exlimi 1822 . . 3  |-  ( E. w  x  e.  w  ->  E. y ( x  e.  y  /\  A. x ( x  e.  y  ->  E. w
( x  e.  w  /\  w  e.  y
) ) ) )
111, 10ax-mp 5 . 2  |-  E. y
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
12 elequ1 1729 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
13 elequ1 1729 . . . . . . . 8  |-  ( z  =  x  ->  (
z  e.  w  <->  x  e.  w ) )
1413anbi1d 687 . . . . . . 7  |-  ( z  =  x  ->  (
( z  e.  w  /\  w  e.  y
)  <->  ( x  e.  w  /\  w  e.  y ) ) )
1514exbidv 1637 . . . . . 6  |-  ( z  =  x  ->  ( E. w ( z  e.  w  /\  w  e.  y )  <->  E. w
( x  e.  w  /\  w  e.  y
) ) )
1612, 15imbi12d 313 . . . . 5  |-  ( z  =  x  ->  (
( z  e.  y  ->  E. w ( z  e.  w  /\  w  e.  y ) )  <->  ( x  e.  y  ->  E. w
( x  e.  w  /\  w  e.  y
) ) ) )
1716cbvalv 1985 . . . 4  |-  ( A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) )  <->  A. x
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
1817anbi2i 677 . . 3  |-  ( ( x  e.  y  /\  A. z ( z  e.  y  ->  E. w
( z  e.  w  /\  w  e.  y
) ) )  <->  ( x  e.  y  /\  A. x
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
1918exbii 1593 . 2  |-  ( E. y ( x  e.  y  /\  A. z
( z  e.  y  ->  E. w ( z  e.  w  /\  w  e.  y ) ) )  <->  E. y ( x  e.  y  /\  A. x
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
2011, 19mpbir 202 1  |-  E. y
( x  e.  y  /\  A. z ( z  e.  y  ->  E. w ( z  e.  w  /\  w  e.  y ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-reg 7563  ax-inf 7596
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-v 2960  df-dif 3325  df-un 3327  df-nul 3631  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator