Theorem fo2nd

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

	Ref	Expression
Assertion	fo2nd	⊢ 2nd : V –onto→ V

Proof

Step	Hyp	Ref	Expression
1		vsnex	⊢ { 𝑥 } ∈ V
2	1	rnex	⊢ ran { 𝑥 } ∈ V
3	2	uniex	⊢ ∪ ran { 𝑥 } ∈ V
4		df-2nd	⊢ 2nd = ( 𝑥 ∈ V ↦ ∪ ran { 𝑥 } )
5	3 4	fnmpti	⊢ 2nd Fn V
6	4	rnmpt	⊢ ran 2nd = { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = ∪ ran { 𝑥 } }
7		vex	⊢ 𝑦 ∈ V
8		opex	⊢ ⟨ 𝑦 , 𝑦 ⟩ ∈ V
9	7 7	op2nda	⊢ ∪ ran { ⟨ 𝑦 , 𝑦 ⟩ } = 𝑦
10	9	eqcomi	⊢ 𝑦 = ∪ ran { ⟨ 𝑦 , 𝑦 ⟩ }
11		sneq	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑦 ⟩ → { 𝑥 } = { ⟨ 𝑦 , 𝑦 ⟩ } )
12	11	rneqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑦 ⟩ → ran { 𝑥 } = ran { ⟨ 𝑦 , 𝑦 ⟩ } )
13	12	unieqd	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑦 ⟩ → ∪ ran { 𝑥 } = ∪ ran { ⟨ 𝑦 , 𝑦 ⟩ } )
14	13	rspceeqv	⊢ ( ( ⟨ 𝑦 , 𝑦 ⟩ ∈ V ∧ 𝑦 = ∪ ran { ⟨ 𝑦 , 𝑦 ⟩ } ) → ∃ 𝑥 ∈ V 𝑦 = ∪ ran { 𝑥 } )
15	8 10 14	mp2an	⊢ ∃ 𝑥 ∈ V 𝑦 = ∪ ran { 𝑥 }
16	7 15	2th	⊢ ( 𝑦 ∈ V ↔ ∃ 𝑥 ∈ V 𝑦 = ∪ ran { 𝑥 } )
17	16	eqabi	⊢ V = { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = ∪ ran { 𝑥 } }
18	6 17	eqtr4i	⊢ ran 2nd = V
19		df-fo	⊢ ( 2nd : V –onto→ V ↔ ( 2nd Fn V ∧ ran 2nd = V ) )
20	5 18 19	mpbir2an	⊢ 2nd : V –onto→ V