Theorem fo1st 7894

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		snex 5367	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7801	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7632	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7874	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6611	. 2 ⊢ 1st Fn V
6	4	rnmpt 5881	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3445	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5396	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6148	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2746	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4579	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5832	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4862	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3584	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 689	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 263	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	abbi2i 2878	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2768	. 2 ⊢ ran 1st = V
19		df-fo 6469	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 708	1 ⊢ 1st :V–onto→V

Syntax hints:   = wceq 1540   ∈ wcel 2105  {cab 2714  ∃wrex 3071  Vcvv 3441  {csn 4569  ⟨cop 4575  ∪ cuni 4848  dom cdm 5605  ran crn 5606   Fn wfn 6458  –onto→wfo 6461  1^st c1st 7872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pr 5365  ax-un 7626

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-fun 6465  df-fn 6466  df-fo 6469  df-1st 7874

This theorem is referenced by:  br1steqg  7896  1stcof  7904  df1st2  7981  1stconst  7983  fsplit  8000  opco1  8006  fpwwe  10472  axpre-sup  10995  homadm  17822  homacd  17823  dmaf  17831  cdaf  17832  1stf1  17976  1stf2  17977  1stfcl  17981  upxp  22845  uptx  22847  cnmpt1st  22890  bcthlem4  24562  uniiccdif  24813  vafval  29073  smfval  29075  0vfval  29076  vsfval  29103  xppreima  31091  xppreima2  31096  1stpreimas  31146  1stpreima  31147  fsuppcurry2  31169  gsummpt2d  31417  cnre2csqima  31967  poimirlem26  35863  poimirlem27  35864