Theorem fo1st 8022

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 5434	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7921	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7751	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 8002	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6703	. 2 ⊢ 1st Fn V
6	4	rnmpt 5960	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3465	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5469	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6235	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2734	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4642	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5911	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4925	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3629	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 690	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 263	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	eqabi 2861	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2756	. 2 ⊢ ran 1st = V
19		df-fo 6559	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 709	1 ⊢ 1st :V–onto→V

Syntax hints:   = wceq 1533   ∈ wcel 2098  {cab 2702  ∃wrex 3059  Vcvv 3461  {csn 4632  ⟨cop 4638  ∪ cuni 4912  dom cdm 5681  ran crn 5682   Fn wfn 6548  –onto→wfo 6551  1^st c1st 8000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pr 5432  ax-un 7745

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5579  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-fun 6555  df-fn 6556  df-fo 6559  df-1st 8002

This theorem is referenced by:  br1steqg  8024  1stcof  8032  df1st2  8111  1stconst  8113  fsplit  8130  opco1  8136  fpwwe  10685  axpre-sup  11208  homadm  18057  homacd  18058  dmaf  18066  cdaf  18067  1stf1  18211  1stf2  18212  1stfcl  18216  upxp  23610  uptx  23612  cnmpt1st  23655  bcthlem4  25338  uniiccdif  25590  precsexlem10  28207  precsexlem11  28208  vafval  30528  smfval  30530  0vfval  30531  vsfval  30558  xppreima  32554  xppreima2  32559  1stpreimas  32608  1stpreima  32609  fsuppcurry2  32631  gsummpt2d  32895  cnre2csqima  33682  poimirlem26  37295  poimirlem27  37296