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

Theorem fo2nd 7861
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 5355 . . . . 5 {𝑥} ∈ V
21rnex 7768 . . . 4 ran {𝑥} ∈ V
32uniex 7603 . . 3 ran {𝑥} ∈ V
4 df-2nd 7841 . . 3 2nd = (𝑥 ∈ V ↦ ran {𝑥})
53, 4fnmpti 6585 . 2 2nd Fn V
64rnmpt 5867 . . 3 ran 2nd = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ran {𝑥}}
7 vex 3437 . . . . 5 𝑦 ∈ V
8 opex 5380 . . . . . 6 𝑦, 𝑦⟩ ∈ V
97, 7op2nda 6136 . . . . . . 7 ran {⟨𝑦, 𝑦⟩} = 𝑦
109eqcomi 2748 . . . . . 6 𝑦 = ran {⟨𝑦, 𝑦⟩}
11 sneq 4572 . . . . . . . . 9 (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
1211rneqd 5850 . . . . . . . 8 (𝑥 = ⟨𝑦, 𝑦⟩ → ran {𝑥} = ran {⟨𝑦, 𝑦⟩})
1312unieqd 4854 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑦⟩ → ran {𝑥} = ran {⟨𝑦, 𝑦⟩})
1413rspceeqv 3576 . . . . . 6 ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ran {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ran {𝑥})
158, 10, 14mp2an 689 . . . . 5 𝑥 ∈ V 𝑦 = ran {𝑥}
167, 152th 263 . . . 4 (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ran {𝑥})
1716abbi2i 2880 . . 3 V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ran {𝑥}}
186, 17eqtr4i 2770 . 2 ran 2nd = V
19 df-fo 6443 . 2 (2nd :V–onto→V ↔ (2nd Fn V ∧ ran 2nd = V))
205, 18, 19mpbir2an 708 1 2nd :V–onto→V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2107  {cab 2716  wrex 3066  Vcvv 3433  {csn 4562  cop 4568   cuni 4840  ran crn 5591   Fn wfn 6432  ontowfo 6435  2nd c2nd 7839
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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-fo 6443  df-2nd 7841
This theorem is referenced by:  br2ndeqg  7863  2ndcof  7871  df2nd2  7948  2ndconst  7950  opco2  7974  iunfo  10304  cdaf  17774  2ndf1  17921  2ndf2  17922  2ndfcl  17924  gsum2dlem2  19581  upxp  22783  uptx  22785  cnmpt2nd  22829  uniiccdif  24751  xppreima  30992  2ndimaxp  30993  2ndresdju  30995  xppreima2  30997  2ndpreima  31049  fsuppcurry1  31069  gsummpt2d  31318  gsumpart  31324  cnre2csqima  31870  filnetlem4  34579
  Copyright terms: Public domain W3C validator