Theorem fo2nd 8046

Description: The 2^nd function maps the universe onto the universe. (Contributed by NM, 14-Oct-2004.) (Revised by Mario Carneiro, 8-Sep-2013.)

Assertion

Ref	Expression
fo2nd	⊢ 2nd :V⟶ontoV

Proof of Theorem fo2nd

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vsnex 5397	. . . . 5 ⊢ {𝑥} ∈ V
2	1	rnex 7946	. . . 4 ⊢ ran {𝑥} ∈ V
3	2	uniex 7782	. . 3 ⊢ ∪ ran {𝑥} ∈ V
4		df-2nd 8026	. . 3 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
5	3, 4	fnmpti 6704	. 2 ⊢ 2nd Fn V
6	4	rnmpt 5946	. . 3 ⊢ ran 2nd = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}}
7		vex 3458	. . . . 5 ⊢ 𝑦 ∈ V
8		opex 5436	. . . . . 6 ⊢ ⟨𝑦, 𝑦⟩ ∈ V
9	7, 7	op2nda 6242	. . . . . . 7 ⊢ ∪ ran {⟨𝑦, 𝑦⟩} = 𝑦
10	9	eqcomi 2772	. . . . . 6 ⊢ 𝑦 = ∪ ran {⟨𝑦, 𝑦⟩}
11		sneq 4594	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → {𝑥} = {⟨𝑦, 𝑦⟩})
12	11	rneqd 5927	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ran {𝑥} = ran {⟨𝑦, 𝑦⟩})
13	12	unieqd 4883	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑦⟩ → ∪ ran {𝑥} = ∪ ran {⟨𝑦, 𝑦⟩})
14	13	rspceeqv 3602	. . . . . 6 ⊢ ((⟨𝑦, 𝑦⟩ ∈ V ∧ 𝑦 = ∪ ran {⟨𝑦, 𝑦⟩}) → ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥})
15	8, 10, 14	mp2an 705	. . . . 5 ⊢ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}
16	7, 15	2th 267	. . . 4 ⊢ (𝑦 ∈ V ↔ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥})
17	16	eqabi 2899	. . 3 ⊢ V = {𝑦 ∣ ∃𝑥 ∈ V 𝑦 = ∪ ran {𝑥}}
18	6, 17	eqtr4i 2789	. 2 ⊢ ran 2nd = V
19		df-fo 6564	. 2 ⊢ (2nd :V⟶ontoV ↔ (2nd Fn V ∧ ran 2nd = V))
20	5, 18, 19	mpbir2an 724	1 ⊢ 2nd :V⟶ontoV

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  {cab 2741  ∃wrex 3090  Vcvv 3454  {csn 4588  ⟨cop 4838  ∪ cuni 4870  ran crn 5656   Fn wfn 6553  ⟶ontowfo 6556  2^nd c2nd 8024

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395  ax-un 7775

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6560  df-fn 6561  df-fo 6564  df-2nd 8026

This theorem is used by:  br2ndeqg  8048  2ndcof  8056  df2nd2  8137  2ndconst  8139  opco2  8162  iunfo  10650  cdaf  18254  2ndf1  18398  2ndf2  18399  2ndfcl  18401  gsum2dlem2  20215  upxp  23972  uptx  23974  cnmpt2nd  24018  uniiccdif  25929  precsexlem10  28632  precsexlem11  28633  xppreima  33311  2ndimaxp  33312  2ndresdju  33315  xppreima2  33317  2ndpreima  33372  fsuppcurry1  33386  gsummpt2d  33680  gsumpart  33694  cnre2csqima  34613  filnetlem4  37347