Theorem fo1st 7709

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 5332	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7616	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7467	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7689	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6491	. 2 ⊢ 1st Fn V
6	4	rnmpt 5827	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3497	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5356	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6082	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2830	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4577	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5774	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4852	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3638	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 690	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 266	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	abbi2i 2953	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2847	. 2 ⊢ ran 1st = V
19		df-fo 6361	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 709	1 ⊢ 1st :V–onto→V

Syntax hints:   = wceq 1537   ∈ wcel 2114  {cab 2799  ∃wrex 3139  Vcvv 3494  {csn 4567  ⟨cop 4573  ∪ cuni 4838  dom cdm 5555  ran crn 5556   Fn wfn 6350  –onto→wfo 6353  1^st c1st 7687

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-fun 6357  df-fn 6358  df-fo 6361  df-1st 7689

This theorem is referenced by:  br1steqg  7711  1stcof  7719  df1st2  7793  1stconst  7795  fsplit  7812  fsplitOLD  7813  algrflem  7819  fpwwe  10068  axpre-sup  10591  homadm  17300  homacd  17301  dmaf  17309  cdaf  17310  1stf1  17442  1stf2  17443  1stfcl  17447  upxp  22231  uptx  22233  cnmpt1st  22276  bcthlem4  23930  uniiccdif  24179  vafval  28380  smfval  28382  0vfval  28383  vsfval  28410  xppreima  30394  xppreima2  30395  1stpreimas  30441  1stpreima  30442  fsuppcurry2  30462  gsummpt2d  30687  cnre2csqima  31154  poimirlem26  34933  poimirlem27  34934