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

Theorem fo2nd 6156
Description: The  2nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)
Assertion
Ref Expression
fo2nd  |-  2nd : _V -onto-> _V

Proof of Theorem fo2nd
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4232 . . . . 5  |-  { x }  e.  _V
21rnex 4958 . . . 4  |-  ran  {
x }  e.  _V
32uniex 4532 . . 3  |-  U. ran  { x }  e.  _V
4 df-2nd 6139 . . 3  |-  2nd  =  ( x  e.  _V  |->  U.
ran  { x } )
53, 4fnmpti 5388 . 2  |-  2nd  Fn  _V
64rnmpt 4941 . . 3  |-  ran  2nd  =  { y  |  E. x  e.  _V  y  =  U. ran  { x } }
7 vex 2804 . . . . 5  |-  y  e. 
_V
8 opex 4253 . . . . . 6  |-  <. y ,  y >.  e.  _V
97, 7op2nda 5173 . . . . . . 7  |-  U. ran  {
<. y ,  y >. }  =  y
109eqcomi 2300 . . . . . 6  |-  y  = 
U. ran  { <. y ,  y >. }
11 sneq 3664 . . . . . . . . . 10  |-  ( x  =  <. y ,  y
>.  ->  { x }  =  { <. y ,  y
>. } )
1211rneqd 4922 . . . . . . . . 9  |-  ( x  =  <. y ,  y
>.  ->  ran  { x }  =  ran  { <. y ,  y >. } )
1312unieqd 3854 . . . . . . . 8  |-  ( x  =  <. y ,  y
>.  ->  U. ran  { x }  =  U. ran  { <. y ,  y >. } )
1413eqeq2d 2307 . . . . . . 7  |-  ( x  =  <. y ,  y
>.  ->  ( y  = 
U. ran  { x } 
<->  y  =  U. ran  {
<. y ,  y >. } ) )
1514rspcev 2897 . . . . . 6  |-  ( (
<. y ,  y >.  e.  _V  /\  y  = 
U. ran  { <. y ,  y >. } )  ->  E. x  e.  _V  y  =  U. ran  {
x } )
168, 10, 15mp2an 653 . . . . 5  |-  E. x  e.  _V  y  =  U. ran  { x }
177, 162th 230 . . . 4  |-  ( y  e.  _V  <->  E. x  e.  _V  y  =  U. ran  { x } )
1817abbi2i 2407 . . 3  |-  _V  =  { y  |  E. x  e.  _V  y  =  U. ran  { x } }
196, 18eqtr4i 2319 . 2  |-  ran  2nd  =  _V
20 df-fo 5277 . 2  |-  ( 2nd
: _V -onto-> _V  <->  ( 2nd  Fn 
_V  /\  ran  2nd  =  _V ) )
215, 19, 20mpbir2an 886 1  |-  2nd : _V -onto-> _V
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   {cab 2282   E.wrex 2557   _Vcvv 2801   {csn 3653   <.cop 3656   U.cuni 3843   ran crn 4706    Fn wfn 5266   -onto->wfo 5269   2ndc2nd 6137
This theorem is referenced by:  2ndcof  6164  df2nd2  6222  2ndconst  6224  iunfo  8177  cdaf  13898  2ndf1  13985  2ndf2  13986  2ndfcl  13988  gsum2d  15239  upxp  17333  uptx  17335  cnmpt2nd  17379  uniiccdif  18949  xppreima  23226  xppreima2  23227  cnre2csqima  23310  br2ndeq  24202  prj3  25183  domrancur1clem  25304  domrancur1c  25305  idval  25828  cmpval  25829  filnetlem4  26433
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-mpt 4095  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-fun 5273  df-fn 5274  df-fo 5277  df-2nd 6139
  Copyright terms: Public domain W3C validator