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

Theorem fo2nd 6602
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 4538 . . . . 5  |-  { x }  e.  _V
21rnex 6517 . . . 4  |-  ran  {
x }  e.  _V
32uniex 6381 . . 3  |-  U. ran  { x }  e.  _V
4 df-2nd 6583 . . 3  |-  2nd  =  ( x  e.  _V  |->  U.
ran  { x } )
53, 4fnmpti 5544 . 2  |-  2nd  Fn  _V
64rnmpt 5090 . . 3  |-  ran  2nd  =  { y  |  E. x  e.  _V  y  =  U. ran  { x } }
7 vex 2980 . . . . 5  |-  y  e. 
_V
8 opex 4561 . . . . . 6  |-  <. y ,  y >.  e.  _V
97, 7op2nda 5329 . . . . . . 7  |-  U. ran  {
<. y ,  y >. }  =  y
109eqcomi 2447 . . . . . 6  |-  y  = 
U. ran  { <. y ,  y >. }
11 sneq 3892 . . . . . . . . . 10  |-  ( x  =  <. y ,  y
>.  ->  { x }  =  { <. y ,  y
>. } )
1211rneqd 5072 . . . . . . . . 9  |-  ( x  =  <. y ,  y
>.  ->  ran  { x }  =  ran  { <. y ,  y >. } )
1312unieqd 4106 . . . . . . . 8  |-  ( x  =  <. y ,  y
>.  ->  U. ran  { x }  =  U. ran  { <. y ,  y >. } )
1413eqeq2d 2454 . . . . . . 7  |-  ( x  =  <. y ,  y
>.  ->  ( y  = 
U. ran  { x } 
<->  y  =  U. ran  {
<. y ,  y >. } ) )
1514rspcev 3078 . . . . . 6  |-  ( (
<. y ,  y >.  e.  _V  /\  y  = 
U. ran  { <. y ,  y >. } )  ->  E. x  e.  _V  y  =  U. ran  {
x } )
168, 10, 15mp2an 672 . . . . 5  |-  E. x  e.  _V  y  =  U. ran  { x }
177, 162th 239 . . . 4  |-  ( y  e.  _V  <->  E. x  e.  _V  y  =  U. ran  { x } )
1817abbi2i 2559 . . 3  |-  _V  =  { y  |  E. x  e.  _V  y  =  U. ran  { x } }
196, 18eqtr4i 2466 . 2  |-  ran  2nd  =  _V
20 df-fo 5429 . 2  |-  ( 2nd
: _V -onto-> _V  <->  ( 2nd  Fn 
_V  /\  ran  2nd  =  _V ) )
215, 19, 20mpbir2an 911 1  |-  2nd : _V -onto-> _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   {cab 2429   E.wrex 2721   _Vcvv 2977   {csn 3882   <.cop 3888   U.cuni 4096   ran crn 4846    Fn wfn 5418   -onto->wfo 5421   2ndc2nd 6581
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 4418  ax-nul 4426  ax-pr 4536  ax-un 6377
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-mpt 4357  df-id 4641  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-fun 5425  df-fn 5426  df-fo 5429  df-2nd 6583
This theorem is referenced by:  2ndcof  6610  df2nd2  6665  2ndconst  6667  iunfo  8708  cdaf  14923  2ndf1  15010  2ndf2  15011  2ndfcl  15013  gsum2dlem2  16467  gsum2dOLD  16469  upxp  19201  uptx  19203  cnmpt2nd  19247  uniiccdif  21063  xppreima  25969  xppreima2  25970  2ndpreima  26007  cnre2csqima  26346  br2ndeq  27591  filnetlem4  28607
  Copyright terms: Public domain W3C validator