Theorem fo1st 8053

Description: The 1^st 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⟶ontoV

Proof of Theorem fo1st

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vsnex 5398	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7953	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7788	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 8033	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6710	. 2 ⊢ 1st Fn V
6	4	rnmpt 5949	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3458	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5437	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6243	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2772	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4594	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5897	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4883	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3602	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 705	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 267	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	eqabi 2899	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2789	. 2 ⊢ ran 1st = V
19		df-fo 6570	. 2 ⊢ (1st :V⟶ontoV ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 724	1 ⊢ 1st :V⟶ontoV

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  {cab 2741  ∃wrex 3090  Vcvv 3454  {csn 4588  ⟨cop 4838  ∪ cuni 4870  dom cdm 5656  ran crn 5657   Fn wfn 6559  ⟶ontowfo 6562  1^st c1st 8031

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396  ax-un 7781

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-fun 6566  df-fn 6567  df-fo 6570  df-1st 8033

This theorem is used by:  br1steqg  8055  1stcof  8063  df1st2  8144  1stconst  8146  fsplit  8163  opco1  8169  fpwwe  10768  axpre-sup  11291  homadm  18256  homacd  18257  dmaf  18265  cdaf  18266  1stf1  18407  1stf2  18408  1stfcl  18412  upxp  23986  uptx  23988  cnmpt1st  24031  bcthlem4  25692  uniiccdif  25943  precsexlem10  28648  precsexlem11  28649  vafval  31251  smfval  31253  0vfval  31254  vsfval  31281  xppreima  33327  xppreima2  33333  1stpreimas  33386  1stpreima  33387  fsuppcurry2  33403  gsummpt2d  33699  cnre2csqima  34647  poimirlem26  38825  poimirlem27  38826