Theorem fo1st 7988

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 5389	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7885	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7717	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7968	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6661	. 2 ⊢ 1st Fn V
6	4	rnmpt 5921	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3451	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5424	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6198	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2738	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4599	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5869	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4884	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3611	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 692	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 264	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	eqabi 2863	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2755	. 2 ⊢ ran 1st = V
19		df-fo 6517	. 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 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  Vcvv 3447  {csn 4589  ⟨cop 4595  ∪ cuni 4871  dom cdm 5638  ran crn 5639   Fn wfn 6506  –onto→wfo 6509  1^st c1st 7966

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-fo 6517  df-1st 7968

This theorem is referenced by:  br1steqg  7990  1stcof  7998  df1st2  8077  1stconst  8079  fsplit  8096  opco1  8102  fpwwe  10599  axpre-sup  11122  homadm  18002  homacd  18003  dmaf  18011  cdaf  18012  1stf1  18153  1stf2  18154  1stfcl  18158  upxp  23510  uptx  23512  cnmpt1st  23555  bcthlem4  25227  uniiccdif  25479  precsexlem10  28118  precsexlem11  28119  vafval  30532  smfval  30534  0vfval  30535  vsfval  30562  xppreima  32569  xppreima2  32575  1stpreimas  32629  1stpreima  32630  fsuppcurry2  32649  gsummpt2d  32989  cnre2csqima  33901  poimirlem26  37640  poimirlem27  37641