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

Theorem zfcndinf 8804
Description: Axiom of Infinity ax-inf 7863, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets above, we are justified in referencing theorem el 4493 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 4493 . . 3  |-  E. w  x  e.  w
2 nfv 1673 . . . . . 6  |-  F/ w  x  e.  y
3 nfe1 1778 . . . . . . . 8  |-  F/ w E. w ( x  e.  w  /\  w  e.  y )
42, 3nfim 1853 . . . . . . 7  |-  F/ w
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) )
54nfal 1873 . . . . . 6  |-  F/ w A. x ( x  e.  y  ->  E. w
( x  e.  w  /\  w  e.  y
) )
62, 5nfan 1861 . . . . 5  |-  F/ w
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
76nfex 1874 . . . 4  |-  F/ w E. y ( x  e.  y  /\  A. x
( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) )
8 axinfnd 8792 . . . . 5  |-  E. y
( x  e.  w  ->  ( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
9819.37aiv 1919 . . . 4  |-  ( x  e.  w  ->  E. y
( x  e.  y  /\  A. x ( x  e.  y  ->  E. w ( x  e.  w  /\  w  e.  y ) ) ) )
107, 9exlimi 1845 . . 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 1759 . . . . . 6  |-  ( z  =  x  ->  (
z  e.  y  <->  x  e.  y ) )
13 elequ1 1759 . . . . . . . 8  |-  ( z  =  x  ->  (
z  e.  w  <->  x  e.  w ) )
1413anbi1d 704 . . . . . . 7  |-  ( z  =  x  ->  (
( z  e.  w  /\  w  e.  y
)  <->  ( x  e.  w  /\  w  e.  y ) ) )
1514exbidv 1680 . . . . . 6  |-  ( z  =  x  ->  ( E. w ( z  e.  w  /\  w  e.  y )  <->  E. w
( x  e.  w  /\  w  e.  y
) ) )
1612, 15imbi12d 320 . . . . 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 1971 . . . 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 694 . . 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 1634 . 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 209 1  |-  E. y
( x  e.  y  /\  A. z ( z  e.  y  ->  E. w ( z  e.  w  /\  w  e.  y ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4432  ax-nul 4440  ax-pow 4489  ax-pr 4550  ax-reg 7826  ax-inf 7863
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2739  df-rex 2740  df-v 2993  df-dif 3350  df-un 3352  df-nul 3657  df-sn 3897  df-pr 3899
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator