Theorem fo1st 7851

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 5354	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7758	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7594	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7831	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6576	. 2 ⊢ 1st Fn V
6	4	rnmpt 5864	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3436	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5379	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6128	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2747	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4571	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5814	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4853	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3575	. . . . . 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 2879	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2769	. 2 ⊢ ran 1st = V
19		df-fo 6439	. 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 1539   ∈ wcel 2106  {cab 2715  ∃wrex 3065  Vcvv 3432  {csn 4561  ⟨cop 4567  ∪ cuni 4839  dom cdm 5589  ran crn 5590   Fn wfn 6428  –onto→wfo 6431  1^st c1st 7829

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-fun 6435  df-fn 6436  df-fo 6439  df-1st 7831

This theorem is referenced by:  br1steqg  7853  1stcof  7861  df1st2  7938  1stconst  7940  fsplit  7957  fsplitOLD  7958  opco1  7964  fpwwe  10402  axpre-sup  10925  homadm  17755  homacd  17756  dmaf  17764  cdaf  17765  1stf1  17909  1stf2  17910  1stfcl  17914  upxp  22774  uptx  22776  cnmpt1st  22819  bcthlem4  24491  uniiccdif  24742  vafval  28965  smfval  28967  0vfval  28968  vsfval  28995  xppreima  30983  xppreima2  30988  1stpreimas  31038  1stpreima  31039  fsuppcurry2  31061  gsummpt2d  31309  cnre2csqima  31861  poimirlem26  35803  poimirlem27  35804