Theorem fo1st 7962

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–onto→V

Proof of Theorem fo1st

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

Step	Hyp	Ref	Expression
1		vsnex 5377	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7860	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7695	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7942	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6641	. 2 ⊢ 1st Fn V
6	4	rnmpt 5912	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3433	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5416	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6189	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2745	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4577	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5860	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4863	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3587	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 693	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 264	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	eqabi 2871	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2762	. 2 ⊢ ran 1st = V
19		df-fo 6504	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 712	1 ⊢ 1st :V–onto→V

Syntax hints:   = wceq 1542   ∈ wcel 2114  {cab 2714  ∃wrex 3061  Vcvv 3429  {csn 4567  ⟨cop 4573  ∪ cuni 4850  dom cdm 5631  ran crn 5632   Fn wfn 6493  –onto→wfo 6496  1^st c1st 7940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-fo 6504  df-1st 7942

This theorem is referenced by:  br1steqg  7964  1stcof  7972  df1st2  8048  1stconst  8050  fsplit  8067  opco1  8073  fpwwe  10569  axpre-sup  11092  homadm  18007  homacd  18008  dmaf  18016  cdaf  18017  1stf1  18158  1stf2  18159  1stfcl  18163  upxp  23588  uptx  23590  cnmpt1st  23633  bcthlem4  25294  uniiccdif  25545  precsexlem10  28208  precsexlem11  28209  vafval  30674  smfval  30676  0vfval  30677  vsfval  30704  xppreima  32718  xppreima2  32724  1stpreimas  32779  1stpreima  32780  fsuppcurry2  32798  gsummpt2d  33110  cnre2csqima  34055  poimirlem26  37967  poimirlem27  37968