This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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