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

Theorem fo2nd 7943
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 š‘„ š‘¦ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vsnex 5387 . . . . 5 {š‘„} āˆˆ V
21rnex 7850 . . . 4 ran {š‘„} āˆˆ V
32uniex 7679 . . 3 āˆŖ ran {š‘„} āˆˆ V
4 df-2nd 7923 . . 3 2nd = (š‘„ āˆˆ V ā†¦ āˆŖ ran {š‘„})
53, 4fnmpti 6645 . 2 2nd Fn V
64rnmpt 5911 . . 3 ran 2nd = {š‘¦ āˆ£ āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ ran {š‘„}}
7 vex 3450 . . . . 5 š‘¦ āˆˆ V
8 opex 5422 . . . . . 6 āŸØš‘¦, š‘¦āŸ© āˆˆ V
97, 7op2nda 6181 . . . . . . 7 āˆŖ ran {āŸØš‘¦, š‘¦āŸ©} = š‘¦
109eqcomi 2746 . . . . . 6 š‘¦ = āˆŖ ran {āŸØš‘¦, š‘¦āŸ©}
11 sneq 4597 . . . . . . . . 9 (š‘„ = āŸØš‘¦, š‘¦āŸ© ā†’ {š‘„} = {āŸØš‘¦, š‘¦āŸ©})
1211rneqd 5894 . . . . . . . 8 (š‘„ = āŸØš‘¦, š‘¦āŸ© ā†’ ran {š‘„} = ran {āŸØš‘¦, š‘¦āŸ©})
1312unieqd 4880 . . . . . . 7 (š‘„ = āŸØš‘¦, š‘¦āŸ© ā†’ āˆŖ ran {š‘„} = āˆŖ ran {āŸØš‘¦, š‘¦āŸ©})
1413rspceeqv 3596 . . . . . 6 ((āŸØš‘¦, š‘¦āŸ© āˆˆ V āˆ§ š‘¦ = āˆŖ ran {āŸØš‘¦, š‘¦āŸ©}) ā†’ āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ ran {š‘„})
158, 10, 14mp2an 691 . . . . 5 āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ ran {š‘„}
167, 152th 264 . . . 4 (š‘¦ āˆˆ V ā†” āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ ran {š‘„})
1716abbi2i 2874 . . 3 V = {š‘¦ āˆ£ āˆƒš‘„ āˆˆ V š‘¦ = āˆŖ ran {š‘„}}
186, 17eqtr4i 2768 . 2 ran 2nd = V
19 df-fo 6503 . 2 (2nd :Vā€“ontoā†’V ā†” (2nd Fn V āˆ§ ran 2nd = V))
205, 18, 19mpbir2an 710 1 2nd :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  ran crn 5635   Fn wfn 6492  ā€“ontoā†’wfo 6495  2nd c2nd 7921
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-2nd 7923
This theorem is referenced by:  br2ndeqg  7945  2ndcof  7953  df2nd2  8032  2ndconst  8034  opco2  8057  iunfo  10476  cdaf  17937  2ndf1  18084  2ndf2  18085  2ndfcl  18087  gsum2dlem2  19749  upxp  22977  uptx  22979  cnmpt2nd  23023  uniiccdif  24945  xppreima  31565  2ndimaxp  31566  2ndresdju  31568  xppreima2  31570  2ndpreima  31624  fsuppcurry1  31645  gsummpt2d  31894  gsumpart  31900  cnre2csqima  32495  filnetlem4  34856
  Copyright terms: Public domain W3C validator