Theorem fo1st 7759

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 5309	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7667	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7507	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7739	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6499	. 2 ⊢ 1st Fn V
6	4	rnmpt 5809	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3402	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5333	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6068	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2745	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4537	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5759	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4819	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3542	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 692	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 267	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	abbi2i 2869	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2762	. 2 ⊢ ran 1st = V
19		df-fo 6364	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 711	1 ⊢ 1st :V–onto→V

Syntax hints:   = wceq 1543   ∈ wcel 2112  {cab 2714  ∃wrex 3052  Vcvv 3398  {csn 4527  ⟨cop 4533  ∪ cuni 4805  dom cdm 5536  ran crn 5537   Fn wfn 6353  –onto→wfo 6356  1^st c1st 7737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-fun 6360  df-fn 6361  df-fo 6364  df-1st 7739

This theorem is referenced by:  br1steqg  7761  1stcof  7769  df1st2  7844  1stconst  7846  fsplit  7863  fsplitOLD  7864  algrflem  7870  fpwwe  10225  axpre-sup  10748  homadm  17500  homacd  17501  dmaf  17509  cdaf  17510  1stf1  17653  1stf2  17654  1stfcl  17658  upxp  22474  uptx  22476  cnmpt1st  22519  bcthlem4  24178  uniiccdif  24429  vafval  28638  smfval  28640  0vfval  28641  vsfval  28668  xppreima  30656  xppreima2  30661  1stpreimas  30712  1stpreima  30713  fsuppcurry2  30735  gsummpt2d  30982  cnre2csqima  31529  poimirlem26  35489  poimirlem27  35490