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

Theorem fo1st 6824
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 4659 . . . . 5  |-  { x }  e.  _V
21dmex 6737 . . . 4  |-  dom  {
x }  e.  _V
32uniex 6598 . . 3  |-  U. dom  { x }  e.  _V
4 df-1st 6804 . . 3  |-  1st  =  ( x  e.  _V  |->  U.
dom  { x } )
53, 4fnmpti 5721 . 2  |-  1st  Fn  _V
64rnmpt 5096 . . 3  |-  ran  1st  =  { y  |  E. x  e.  _V  y  =  U. dom  { x } }
7 vex 3084 . . . . 5  |-  y  e. 
_V
8 opex 4682 . . . . . 6  |-  <. y ,  y >.  e.  _V
97, 7op1sta 5334 . . . . . . 7  |-  U. dom  {
<. y ,  y >. }  =  y
109eqcomi 2435 . . . . . 6  |-  y  = 
U. dom  { <. y ,  y >. }
11 sneq 4006 . . . . . . . . . 10  |-  ( x  =  <. y ,  y
>.  ->  { x }  =  { <. y ,  y
>. } )
1211dmeqd 5053 . . . . . . . . 9  |-  ( x  =  <. y ,  y
>.  ->  dom  { x }  =  dom  { <. y ,  y >. } )
1312unieqd 4226 . . . . . . . 8  |-  ( x  =  <. y ,  y
>.  ->  U. dom  { x }  =  U. dom  { <. y ,  y >. } )
1413eqeq2d 2436 . . . . . . 7  |-  ( x  =  <. y ,  y
>.  ->  ( y  = 
U. dom  { x } 
<->  y  =  U. dom  {
<. y ,  y >. } ) )
1514rspcev 3182 . . . . . 6  |-  ( (
<. y ,  y >.  e.  _V  /\  y  = 
U. dom  { <. y ,  y >. } )  ->  E. x  e.  _V  y  =  U. dom  {
x } )
168, 10, 15mp2an 676 . . . . 5  |-  E. x  e.  _V  y  =  U. dom  { x }
177, 162th 242 . . . 4  |-  ( y  e.  _V  <->  E. x  e.  _V  y  =  U. dom  { x } )
1817abbi2i 2555 . . 3  |-  _V  =  { y  |  E. x  e.  _V  y  =  U. dom  { x } }
196, 18eqtr4i 2454 . 2  |-  ran  1st  =  _V
20 df-fo 5604 . 2  |-  ( 1st
: _V -onto-> _V  <->  ( 1st  Fn 
_V  /\  ran  1st  =  _V ) )
215, 19, 20mpbir2an 928 1  |-  1st : _V -onto-> _V
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1868   {cab 2407   E.wrex 2776   _Vcvv 3081   {csn 3996   <.cop 4002   U.cuni 4216   dom cdm 4850   ran crn 4851    Fn wfn 5593   -onto->wfo 5596   1stc1st 6802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657  ax-un 6594
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-fun 5600  df-fn 5601  df-fo 5604  df-1st 6804
This theorem is referenced by:  1stcof  6832  df1st2  6890  1stconst  6892  fsplit  6909  algrflem  6913  fpwwe  9072  axpre-sup  9594  homadm  15923  homacd  15924  dmaf  15932  cdaf  15933  1stf1  16065  1stf2  16066  1stfcl  16070  upxp  20625  uptx  20627  cnmpt1st  20670  bcthlem4  22282  uniiccdif  22522  vafval  26208  smfval  26210  0vfval  26211  vsfval  26240  xppreima  28238  xppreima2  28239  1stpreimas  28276  1stpreima  28277  gsummpt2d  28539  cnre2csqima  28713  br1steq  30409  poimirlem26  31880  poimirlem27  31881
  Copyright terms: Public domain W3C validator