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

Theorem fo1st 7565
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 5223 . . . . 5 {𝑥} ∈ V
21dmex 7472 . . . 4 dom {𝑥} ∈ V
32uniex 7323 . . 3 dom {𝑥} ∈ V
4 df-1st 7545 . . 3 1st = (𝑥 ∈ V ↦ dom {𝑥})
53, 4fnmpti 6359 . 2 1st Fn V
64rnmpt 5709 . . 3 ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
7 vex 3440 . . . . 5 𝑦 ∈ V
8 opex 5248 . . . . . 6 𝑦, 𝑦⟩ ∈ V
97, 7op1sta 5957 . . . . . . 7 dom {⟨𝑦, 𝑦⟩} = 𝑦
109eqcomi 2804 . . . . . 6 𝑦 = dom {⟨𝑦, 𝑦⟩}
11 sneq 4482 . . . . . . . . 9 (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
1211dmeqd 5660 . . . . . . . 8 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1312unieqd 4755 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1413rspceeqv 3577 . . . . . 6 ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = dom {𝑥})
158, 10, 14mp2an 688 . . . . 5 𝑥 ∈ V 𝑦 = dom {𝑥}
167, 152th 265 . . . 4 (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = dom {𝑥})
1716abbi2i 2922 . . 3 V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
186, 17eqtr4i 2822 . 2 ran 1st = V
19 df-fo 6231 . 2 (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
205, 18, 19mpbir2an 707 1 1st :V–onto→V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1522  wcel 2081  {cab 2775  wrex 3106  Vcvv 3437  {csn 4472  cop 4478   cuni 4745  dom cdm 5443  ran crn 5444   Fn wfn 6220  ontowfo 6223  1st c1st 7543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-fun 6227  df-fn 6228  df-fo 6231  df-1st 7545
This theorem is referenced by:  br1steqg  7567  1stcof  7575  df1st2  7649  1stconst  7651  fsplit  7668  algrflem  7672  fpwwe  9914  axpre-sup  10437  homadm  17129  homacd  17130  dmaf  17138  cdaf  17139  1stf1  17271  1stf2  17272  1stfcl  17276  upxp  21915  uptx  21917  cnmpt1st  21960  bcthlem4  23613  uniiccdif  23862  vafval  28071  smfval  28073  0vfval  28074  vsfval  28101  xppreima  30084  xppreima2  30085  1stpreimas  30129  1stpreima  30130  fsuppcurry2  30150  gsummpt2d  30496  cnre2csqima  30771  poimirlem26  34468  poimirlem27  34469
  Copyright terms: Public domain W3C validator