Theorem fo1st 7565

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 5223	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7472	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7323	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7545	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6359	. 2 ⊢ 1st Fn V
6	4	rnmpt 5709	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3440	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5248	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 5957	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2804	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4482	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5660	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4755	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3577	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 688	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 265	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	abbi2i 2922	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2822	. 2 ⊢ ran 1st = V
19		df-fo 6231	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 707	1 ⊢ 1st :V–onto→V

Syntax hints:   = wceq 1522   ∈ wcel 2081  {cab 2775  ∃wrex 3106  Vcvv 3437  {csn 4472  ⟨cop 4478  ∪ cuni 4745  dom cdm 5443  ran crn 5444   Fn wfn 6220  –onto→wfo 6223  1^st c1st 7543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-fun 6227  df-fn 6228  df-fo 6231  df-1st 7545

This theorem is referenced by:  br1steqg  7567  1stcof  7575  df1st2  7649  1stconst  7651  fsplit  7668  algrflem  7672  fpwwe  9914  axpre-sup  10437  homadm  17129  homacd  17130  dmaf  17138  cdaf  17139  1stf1  17271  1stf2  17272  1stfcl  17276  upxp  21915  uptx  21917  cnmpt1st  21960  bcthlem4  23613  uniiccdif  23862  vafval  28071  smfval  28073  0vfval  28074  vsfval  28101  xppreima  30084  xppreima2  30085  1stpreimas  30129  1stpreima  30130  fsuppcurry2  30150  gsummpt2d  30496  cnre2csqima  30771  poimirlem26  34468  poimirlem27  34469