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

Theorem fo1st 8022
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 5434 . . . . 5 {𝑥} ∈ V
21dmex 7921 . . . 4 dom {𝑥} ∈ V
32uniex 7751 . . 3 dom {𝑥} ∈ V
4 df-1st 8002 . . 3 1st = (𝑥 ∈ V ↦ dom {𝑥})
53, 4fnmpti 6703 . 2 1st Fn V
64rnmpt 5960 . . 3 ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
7 vex 3465 . . . . 5 𝑦 ∈ V
8 opex 5469 . . . . . 6 𝑦, 𝑦⟩ ∈ V
97, 7op1sta 6235 . . . . . . 7 dom {⟨𝑦, 𝑦⟩} = 𝑦
109eqcomi 2734 . . . . . 6 𝑦 = dom {⟨𝑦, 𝑦⟩}
11 sneq 4642 . . . . . . . . 9 (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
1211dmeqd 5911 . . . . . . . 8 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1312unieqd 4925 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1413rspceeqv 3629 . . . . . 6 ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = dom {𝑥})
158, 10, 14mp2an 690 . . . . 5 𝑥 ∈ V 𝑦 = dom {𝑥}
167, 152th 263 . . . 4 (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = dom {𝑥})
1716eqabi 2861 . . 3 V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
186, 17eqtr4i 2756 . 2 ran 1st = V
19 df-fo 6559 . 2 (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
205, 18, 19mpbir2an 709 1 1st :V–onto→V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wcel 2098  {cab 2702  wrex 3059  Vcvv 3461  {csn 4632  cop 4638   cuni 4912  dom cdm 5681  ran crn 5682   Fn wfn 6548  ontowfo 6551  1st c1st 8000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-fun 6555  df-fn 6556  df-fo 6559  df-1st 8002
This theorem is referenced by:  br1steqg  8024  1stcof  8032  df1st2  8111  1stconst  8113  fsplit  8130  opco1  8136  fpwwe  10685  axpre-sup  11208  homadm  18057  homacd  18058  dmaf  18066  cdaf  18067  1stf1  18211  1stf2  18212  1stfcl  18216  upxp  23610  uptx  23612  cnmpt1st  23655  bcthlem4  25338  uniiccdif  25590  precsexlem10  28207  precsexlem11  28208  vafval  30528  smfval  30530  0vfval  30531  vsfval  30558  xppreima  32554  xppreima2  32559  1stpreimas  32608  1stpreima  32609  fsuppcurry2  32631  gsummpt2d  32895  cnre2csqima  33682  poimirlem26  37295  poimirlem27  37296
  Copyright terms: Public domain W3C validator