Theorem fo1st 8006

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 5400	. . . . 5 ⊢ {𝑥} ∈ V
2	1	dmex 7906	. . . 4 ⊢ dom {𝑥} ∈ V
3	2	uniex 7743	. . 3 ⊢ ∪ dom {𝑥} ∈ V
4		df-1st 7986	. . 3 ⊢ 1st = (𝑥 ∈ V ↦ ∪ dom {𝑥})
5	3, 4	fnmpti 6675	. 2 ⊢ 1st Fn V
6	4	rnmpt 5941	. . 3 ⊢ ran 1st = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
7		vex 3454	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5439	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op1sta 6221	. . . . . . 7 ⊢ ∪ dom {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2769	. . . . . 6 ⊢ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}
11		sneq 4594	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	dmeqd 5889	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → dom {𝑥} = dom {⟨𝑦, 𝑦⟩})
13	12	unieqd 4880	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ dom {𝑥} = ∪ dom {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3599	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ dom {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
15	8, 10, 14	mp2an 705	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}
16	7, 15	2th 267	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥})
17	16	eqabi 2895	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ dom {𝑥}}
18	6, 17	eqtr4i 2786	. 2 ⊢ ran 1st = V
19		df-fo 6539	. 2 ⊢ (1st :V–onto→V ↔ (1st Fn V ∧ ran 1st = V))
20	5, 18, 19	mpbir2an 724	1 ⊢ 1st :V–onto→V

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  {cab 2738  ∃wrex 3086  Vcvv 3450  {csn 4584  ⟨cop 4590  ∪ cuni 4867  dom cdm 5655  ran crn 5656   Fn wfn 6528  –onto→wfo 6531  1^st c1st 7984

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6535  df-fn 6536  df-fo 6539  df-1st 7986

This theorem is used by:  br1steqg  8008  1stcof  8016  df1st2  8095  1stconst  8097  fsplit  8114  opco1  8120  fpwwe  10655  axpre-sup  11178  homadm  18129  homacd  18130  dmaf  18138  cdaf  18139  1stf1  18280  1stf2  18281  1stfcl  18285  upxp  23849  uptx  23851  cnmpt1st  23894  bcthlem4  25555  uniiccdif  25806  precsexlem10  28481  precsexlem11  28482  vafval  31084  smfval  31086  0vfval  31087  vsfval  31114  xppreima  33118  xppreima2  33124  1stpreimas  33178  1stpreima  33179  fsuppcurry2  33196  gsummpt2d  33489  cnre2csqima  34421  poimirlem26  38395  poimirlem27  38396