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

Theorem fo1st 7942
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 š‘„ š‘¦ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vsnex 5387 . . . . 5 {š‘„} āˆˆ V
21dmex 7849 . . . 4 dom {š‘„} āˆˆ V
32uniex 7679 . . 3 āˆŖ dom {š‘„} āˆˆ V
4 df-1st 7922 . . 3 1st = (š‘„ āˆˆ V ā†¦ āˆŖ dom {š‘„})
53, 4fnmpti 6645 . 2 1st Fn V
64rnmpt 5911 . . 3 ran 1st = {š‘¦ āˆ£ āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ dom {š‘„}}
7 vex 3450 . . . . 5 š‘¦ āˆˆ V
8 opex 5422 . . . . . 6 āŸØš‘¦, š‘¦āŸ© āˆˆ V
97, 7op1sta 6178 . . . . . . 7 āˆŖ dom {āŸØš‘¦, š‘¦āŸ©} = š‘¦
109eqcomi 2746 . . . . . 6 š‘¦ = āˆŖ dom {āŸØš‘¦, š‘¦āŸ©}
11 sneq 4597 . . . . . . . . 9 (š‘„ = āŸØš‘¦, š‘¦āŸ© ā†’ {š‘„} = {āŸØš‘¦, š‘¦āŸ©})
1211dmeqd 5862 . . . . . . . 8 (š‘„ = āŸØš‘¦, š‘¦āŸ© ā†’ dom {š‘„} = dom {āŸØš‘¦, š‘¦āŸ©})
1312unieqd 4880 . . . . . . 7 (š‘„ = āŸØš‘¦, š‘¦āŸ© ā†’ āˆŖ dom {š‘„} = āˆŖ dom {āŸØš‘¦, š‘¦āŸ©})
1413rspceeqv 3596 . . . . . 6 ((āŸØš‘¦, š‘¦āŸ© āˆˆ V āˆ§ š‘¦ = āˆŖ dom {āŸØš‘¦, š‘¦āŸ©}) ā†’ āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ dom {š‘„})
158, 10, 14mp2an 691 . . . . 5 āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ dom {š‘„}
167, 152th 264 . . . 4 (š‘¦ āˆˆ V ā†” āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ dom {š‘„})
1716abbi2i 2874 . . 3 V = {š‘¦ āˆ£ āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ dom {š‘„}}
186, 17eqtr4i 2768 . 2 ran 1st = V
19 df-fo 6503 . 2 (1st :Vā€“ontoā†’V ā†” (1st Fn V āˆ§ ran 1st = V))
205, 18, 19mpbir2an 710 1 1st :Vā€“ontoā†’V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   āˆˆ wcel 2107  {cab 2714  āˆƒwrex 3074  Vcvv 3446  {csn 4587  āŸØcop 4593  āˆŖ cuni 4866  dom cdm 5634  ran crn 5635   Fn wfn 6492  ā€“ontoā†’wfo 6495  1st c1st 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-fun 6499  df-fn 6500  df-fo 6503  df-1st 7922
This theorem is referenced by:  br1steqg  7944  1stcof  7952  df1st2  8031  1stconst  8033  fsplit  8050  opco1  8056  fpwwe  10583  axpre-sup  11106  homadm  17927  homacd  17928  dmaf  17936  cdaf  17937  1stf1  18081  1stf2  18082  1stfcl  18086  upxp  22977  uptx  22979  cnmpt1st  23022  bcthlem4  24694  uniiccdif  24945  vafval  29548  smfval  29550  0vfval  29551  vsfval  29578  xppreima  31565  xppreima2  31570  1stpreimas  31622  1stpreima  31623  fsuppcurry2  31646  gsummpt2d  31894  cnre2csqima  32495  poimirlem26  36107  poimirlem27  36108
  Copyright terms: Public domain W3C validator