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

Theorem zfcndinf 8427
Description: Axiom of Infinity ax-inf 7527, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing theorem el 4323 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 4323 . . 3  |-  E. w  x  e.  w
2 nfv 1626 . . . . . 6  |-  F/ w  x  e.  y
3 nfe1 1739 . . . . . . . 8  |-  F/ w E. w ( x  e.  w  /\  w  e.  y )
42, 3nfim 1822 . . . . . . 7  |-  F/ w
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) )
54nfal 1854 . . . . . 6  |-  F/ w A. x ( x  e.  y  ->  E. w
( x  e.  w  /\  w  e.  y
) )
62, 5nfan 1836 . . . . 5  |-  F/ w
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
76nfex 1855 . . . 4  |-  F/ w E. y ( x  e.  y  /\  A. x
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
8 axinfnd 8415 . . . . 5  |-  E. y
( x  e.  w  ->  ( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
9819.37aiv 1912 . . . 4  |-  ( x  e.  w  ->  E. y
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
107, 9exlimi 1811 . . 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 8 . 2  |-  E. y
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
12 elequ1 1720 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
13 elequ1 1720 . . . . . . . 8  |-  ( z  =  x  ->  (
z  e.  w  <->  x  e.  w ) )
1413anbi1d 686 . . . . . . 7  |-  ( z  =  x  ->  (
( z  e.  w  /\  w  e.  y
)  <->  ( x  e.  w  /\  w  e.  y ) ) )
1514exbidv 1633 . . . . . 6  |-  ( z  =  x  ->  ( E. w ( z  e.  w  /\  w  e.  y )  <->  E. w
( x  e.  w  /\  w  e.  y
) ) )
1612, 15imbi12d 312 . . . . 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 2037 . . . 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 676 . . 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 1589 . 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 201 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 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-reg 7494  ax-inf 7527
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-v 2902  df-dif 3267  df-un 3269  df-nul 3573  df-sn 3764  df-pr 3765
  Copyright terms: Public domain W3C validator