Theorem fo2nd 5704

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–onto→V

Proof of Theorem fo2nd

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2534	. . . . . 6 ⊢ x ∈ V
2		snexgOLD 3905	. . . . . 6 ⊢ (x ∈ V → {x} ∈ V)
3	1, 2	ax-mp 7	. . . . 5 ⊢ {x} ∈ V
4	3	rnex 4522	. . . 4 ⊢ ran {x} ∈ V
5	4	uniex 4120	. . 3 ⊢ ∪ ran {x} ∈ V
6		df-2nd 5687	. . 3 ⊢ 2nd = (x ∈ V ↦ ∪ ran {x})
7	5, 6	fnmpti 4949	. 2 ⊢ 2nd Fn V
8	6	rnmpt 4505	. . 3 ⊢ ran 2nd = {y ∣ ∃x ∈ V y = ∪ ran {x}}
9		vex 2534	. . . . 5 ⊢ y ∈ V
10	9, 9	opex 3936	. . . . . 6 ⊢ ⟨y, y⟩ ∈ V
11	9, 9	op2nda 4728	. . . . . . 7 ⊢ ∪ ran {⟨y, y⟩} = y
12	11	eqcomi 2022	. . . . . 6 ⊢ y = ∪ ran {⟨y, y⟩}
13		sneq 3357	. . . . . . . . . 10 ⊢ (x = ⟨y, y⟩ → {x} = {⟨y, y⟩})
14	13	rneqd 4486	. . . . . . . . 9 ⊢ (x = ⟨y, y⟩ → ran {x} = ran {⟨y, y⟩})
15	14	unieqd 3561	. . . . . . . 8 ⊢ (x = ⟨y, y⟩ → ∪ ran {x} = ∪ ran {⟨y, y⟩})
16	15	eqeq2d 2029	. . . . . . 7 ⊢ (x = ⟨y, y⟩ → (y = ∪ ran {x} ↔ y = ∪ ran {⟨y, y⟩}))
17	16	rspcev 2629	. . . . . 6 ⊢ ((⟨y, y⟩ ∈ V ∧ y = ∪ ran {⟨y, y⟩}) → ∃x ∈ V y = ∪ ran {x})
18	10, 12, 17	mp2an 404	. . . . 5 ⊢ ∃x ∈ V y = ∪ ran {x}
19	9, 18	2th 163	. . . 4 ⊢ (y ∈ V ↔ ∃x ∈ V y = ∪ ran {x})
20	19	abbi2i 2130	. . 3 ⊢ V = {y ∣ ∃x ∈ V y = ∪ ran {x}}
21	8, 20	eqtr4i 2041	. 2 ⊢ ran 2nd = V
22		df-fo 4831	. 2 ⊢ (2nd :V–onto→V ↔ (2nd Fn V ∧ ran 2nd = V))
23	7, 21, 22	mpbir2an 835	1 ⊢ 2nd :V–onto→V

Syntax hints:   = wceq 1226   ∈ wcel 1370  {cab 2004  ∃wrex 2281  Vcvv 2531  {csn 3346  ⟨cop 3349  ∪ cuni 3550  ran crn 4269   Fn wfn 4820  –onto→wfo 4823  2^nd c2nd 5685

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-un 4116

This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-mpt 3790  df-id 4000  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-fun 4827  df-fn 4828  df-fo 4831  df-2nd 5687

This theorem is referenced by:  2ndcof  5710  2ndexg  5714  df2nd2  5760  2ndconst  5762