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

Theorem fo1st 7133
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 snex 4869 . . . . 5 {𝑥} ∈ V
21dmex 7046 . . . 4 dom {𝑥} ∈ V
32uniex 6906 . . 3 dom {𝑥} ∈ V
4 df-1st 7113 . . 3 1st = (𝑥 ∈ V ↦ dom {𝑥})
53, 4fnmpti 5979 . 2 1st Fn V
64rnmpt 5331 . . 3 ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
7 vex 3189 . . . . 5 𝑦 ∈ V
8 opex 4893 . . . . . 6 𝑦, 𝑦⟩ ∈ V
97, 7op1sta 5576 . . . . . . 7 dom {⟨𝑦, 𝑦⟩} = 𝑦
109eqcomi 2630 . . . . . 6 𝑦 = dom {⟨𝑦, 𝑦⟩}
11 sneq 4158 . . . . . . . . . 10 (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
1211dmeqd 5286 . . . . . . . . 9 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1312unieqd 4412 . . . . . . . 8 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1413eqeq2d 2631 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑦⟩ → (𝑦 = dom {𝑥} ↔ 𝑦 = dom {⟨𝑦, 𝑦⟩}))
1514rspcev 3295 . . . . . 6 ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = dom {𝑥})
168, 10, 15mp2an 707 . . . . 5 𝑥 ∈ V 𝑦 = dom {𝑥}
177, 162th 254 . . . 4 (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = dom {𝑥})
1817abbi2i 2735 . . 3 V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
196, 18eqtr4i 2646 . 2 ran 1st = V
20 df-fo 5853 . 2 (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
215, 19, 20mpbir2an 954 1 1st :V–onto→V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  {cab 2607  wrex 2908  Vcvv 3186  {csn 4148  cop 4154   cuni 4402  dom cdm 5074  ran crn 5075   Fn wfn 5842  ontowfo 5845  1st c1st 7111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-fun 5849  df-fn 5850  df-fo 5853  df-1st 7113
This theorem is referenced by:  1stcof  7141  df1st2  7208  1stconst  7210  fsplit  7227  algrflem  7231  fpwwe  9412  axpre-sup  9934  homadm  16611  homacd  16612  dmaf  16620  cdaf  16621  1stf1  16753  1stf2  16754  1stfcl  16758  upxp  21336  uptx  21338  cnmpt1st  21381  bcthlem4  23032  uniiccdif  23252  vafval  27307  smfval  27309  0vfval  27310  vsfval  27337  xppreima  29291  xppreima2  29292  1stpreimas  29326  1stpreima  29327  gsummpt2d  29566  cnre2csqima  29739  br1steq  31374  poimirlem26  33067  poimirlem27  33068
  Copyright terms: Public domain W3C validator