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

Theorem fo2nd 7714
 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 snex 5300 . . . . 5 {𝑥} ∈ V
21rnex 7622 . . . 4 ran {𝑥} ∈ V
32uniex 7465 . . 3 ran {𝑥} ∈ V
4 df-2nd 7694 . . 3 2nd = (𝑥 ∈ V ↦ ran {𝑥})
53, 4fnmpti 6474 . 2 2nd Fn V
64rnmpt 5796 . . 3 ran 2nd = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ran {𝑥}}
7 vex 3413 . . . . 5 𝑦 ∈ V
8 opex 5324 . . . . . 6 𝑦, 𝑦⟩ ∈ V
97, 7op2nda 6057 . . . . . . 7 ran {⟨𝑦, 𝑦⟩} = 𝑦
109eqcomi 2767 . . . . . 6 𝑦 = ran {⟨𝑦, 𝑦⟩}
11 sneq 4532 . . . . . . . . 9 (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
1211rneqd 5779 . . . . . . . 8 (𝑥 = ⟨𝑦, 𝑦⟩ → ran {𝑥} = ran {⟨𝑦, 𝑦⟩})
1312unieqd 4812 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑦⟩ → ran {𝑥} = ran {⟨𝑦, 𝑦⟩})
1413rspceeqv 3556 . . . . . 6 ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ran {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ran {𝑥})
158, 10, 14mp2an 691 . . . . 5 𝑥 ∈ V 𝑦 = ran {𝑥}
167, 152th 267 . . . 4 (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ran {𝑥})
1716abbi2i 2891 . . 3 V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ran {𝑥}}
186, 17eqtr4i 2784 . 2 ran 2nd = V
19 df-fo 6341 . 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 1538   ∈ wcel 2111  {cab 2735  ∃wrex 3071  Vcvv 3409  {csn 4522  ⟨cop 4528  ∪ cuni 4798  ran crn 5525   Fn wfn 6330  –onto→wfo 6333  2nd c2nd 7692 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-fun 6337  df-fn 6338  df-fo 6341  df-2nd 7694 This theorem is referenced by:  br2ndeqg  7716  2ndcof  7724  df2nd2  7799  2ndconst  7801  iunfo  9999  cdaf  17376  2ndf1  17511  2ndf2  17512  2ndfcl  17514  gsum2dlem2  19159  upxp  22323  uptx  22325  cnmpt2nd  22369  uniiccdif  24278  xppreima  30506  2ndimaxp  30507  2ndresdju  30509  xppreima2  30511  2ndpreima  30564  fsuppcurry1  30584  gsummpt2d  30835  gsumpart  30841  cnre2csqima  31382  filnetlem4  34119
 Copyright terms: Public domain W3C validator