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

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

Proof of Theorem fo1st
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4678 . . . . 5  |-  { x }  e.  _V
21dmex 6706 . . . 4  |-  dom  {
x }  e.  _V
32uniex 6569 . . 3  |-  U. dom  { x }  e.  _V
4 df-1st 6773 . . 3  |-  1st  =  ( x  e.  _V  |->  U.
dom  { x } )
53, 4fnmpti 5691 . 2  |-  1st  Fn  _V
64rnmpt 5237 . . 3  |-  ran  1st  =  { y  |  E. x  e.  _V  y  =  U. dom  { x } }
7 vex 3109 . . . . 5  |-  y  e. 
_V
8 opex 4701 . . . . . 6  |-  <. y ,  y >.  e.  _V
97, 7op1sta 5473 . . . . . . 7  |-  U. dom  {
<. y ,  y >. }  =  y
109eqcomi 2467 . . . . . 6  |-  y  = 
U. dom  { <. y ,  y >. }
11 sneq 4026 . . . . . . . . . 10  |-  ( x  =  <. y ,  y
>.  ->  { x }  =  { <. y ,  y
>. } )
1211dmeqd 5194 . . . . . . . . 9  |-  ( x  =  <. y ,  y
>.  ->  dom  { x }  =  dom  { <. y ,  y >. } )
1312unieqd 4245 . . . . . . . 8  |-  ( x  =  <. y ,  y
>.  ->  U. dom  { x }  =  U. dom  { <. y ,  y >. } )
1413eqeq2d 2468 . . . . . . 7  |-  ( x  =  <. y ,  y
>.  ->  ( y  = 
U. dom  { x } 
<->  y  =  U. dom  {
<. y ,  y >. } ) )
1514rspcev 3207 . . . . . 6  |-  ( (
<. y ,  y >.  e.  _V  /\  y  = 
U. dom  { <. y ,  y >. } )  ->  E. x  e.  _V  y  =  U. dom  {
x } )
168, 10, 15mp2an 670 . . . . 5  |-  E. x  e.  _V  y  =  U. dom  { x }
177, 162th 239 . . . 4  |-  ( y  e.  _V  <->  E. x  e.  _V  y  =  U. dom  { x } )
1817abbi2i 2587 . . 3  |-  _V  =  { y  |  E. x  e.  _V  y  =  U. dom  { x } }
196, 18eqtr4i 2486 . 2  |-  ran  1st  =  _V
20 df-fo 5576 . 2  |-  ( 1st
: _V -onto-> _V  <->  ( 1st  Fn 
_V  /\  ran  1st  =  _V ) )
215, 19, 20mpbir2an 918 1  |-  1st : _V -onto-> _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823   {cab 2439   E.wrex 2805   _Vcvv 3106   {csn 4016   <.cop 4022   U.cuni 4235   dom cdm 4988   ran crn 4989    Fn wfn 5565   -onto->wfo 5568   1stc1st 6771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-fun 5572  df-fn 5573  df-fo 5576  df-1st 6773
This theorem is referenced by:  1stcof  6801  df1st2  6859  1stconst  6861  fsplit  6878  algrflem  6882  fpwwe  9013  axpre-sup  9535  homadm  15518  homacd  15519  dmaf  15527  cdaf  15528  1stf1  15660  1stf2  15661  1stfcl  15665  upxp  20290  uptx  20292  cnmpt1st  20335  bcthlem4  21932  uniiccdif  22153  vafval  25694  smfval  25696  0vfval  25697  vsfval  25726  xppreima  27708  xppreima2  27709  1stpreimas  27752  1stpreima  27753  gsummpt2d  28006  cnre2csqima  28128  br1steq  29444
  Copyright terms: Public domain W3C validator