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

Theorem fo1st 8032
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 5439 . . . . 5 {𝑥} ∈ V
21dmex 7931 . . . 4 dom {𝑥} ∈ V
32uniex 7759 . . 3 dom {𝑥} ∈ V
4 df-1st 8012 . . 3 1st = (𝑥 ∈ V ↦ dom {𝑥})
53, 4fnmpti 6711 . 2 1st Fn V
64rnmpt 5970 . . 3 ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
7 vex 3481 . . . . 5 𝑦 ∈ V
8 opex 5474 . . . . . 6 𝑦, 𝑦⟩ ∈ V
97, 7op1sta 6246 . . . . . . 7 dom {⟨𝑦, 𝑦⟩} = 𝑦
109eqcomi 2743 . . . . . 6 𝑦 = dom {⟨𝑦, 𝑦⟩}
11 sneq 4640 . . . . . . . . 9 (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
1211dmeqd 5918 . . . . . . . 8 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1312unieqd 4924 . . . . . . 7 (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
1413rspceeqv 3644 . . . . . 6 ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = dom {𝑥})
158, 10, 14mp2an 692 . . . . 5 𝑥 ∈ V 𝑦 = dom {𝑥}
167, 152th 264 . . . 4 (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = dom {𝑥})
1716eqabi 2874 . . 3 V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = dom {𝑥}}
186, 17eqtr4i 2765 . 2 ran 1st = V
19 df-fo 6568 . 2 (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
205, 18, 19mpbir2an 711 1 1st :V–onto→V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1536  wcel 2105  {cab 2711  wrex 3067  Vcvv 3477  {csn 4630  cop 4636   cuni 4911  dom cdm 5688  ran crn 5689   Fn wfn 6557  ontowfo 6560  1st c1st 8010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-fo 6568  df-1st 8012
This theorem is referenced by:  br1steqg  8034  1stcof  8042  df1st2  8121  1stconst  8123  fsplit  8140  opco1  8146  fpwwe  10683  axpre-sup  11206  homadm  18093  homacd  18094  dmaf  18102  cdaf  18103  1stf1  18247  1stf2  18248  1stfcl  18252  upxp  23646  uptx  23648  cnmpt1st  23691  bcthlem4  25374  uniiccdif  25626  precsexlem10  28254  precsexlem11  28255  vafval  30631  smfval  30633  0vfval  30634  vsfval  30661  xppreima  32661  xppreima2  32667  1stpreimas  32720  1stpreima  32721  fsuppcurry2  32743  gsummpt2d  33034  cnre2csqima  33871  poimirlem26  37632  poimirlem27  37633
  Copyright terms: Public domain W3C validator