Metamath Proof Explorer


Theorem 2ndval

Description: The value of the function that extracts the second member of an ordered pair. (Contributed by NM, 9-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion 2ndval ( 2nd𝐴 ) = ran { 𝐴 }

Proof

Step Hyp Ref Expression
1 sneq ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
2 1 rneqd ( 𝑥 = 𝐴 → ran { 𝑥 } = ran { 𝐴 } )
3 2 unieqd ( 𝑥 = 𝐴 ran { 𝑥 } = ran { 𝐴 } )
4 df-2nd 2nd = ( 𝑥 ∈ V ↦ ran { 𝑥 } )
5 snex { 𝐴 } ∈ V
6 5 rnex ran { 𝐴 } ∈ V
7 6 uniex ran { 𝐴 } ∈ V
8 3 4 7 fvmpt ( 𝐴 ∈ V → ( 2nd𝐴 ) = ran { 𝐴 } )
9 fvprc ( ¬ 𝐴 ∈ V → ( 2nd𝐴 ) = ∅ )
10 snprc ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
11 10 biimpi ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
12 11 rneqd ( ¬ 𝐴 ∈ V → ran { 𝐴 } = ran ∅ )
13 rn0 ran ∅ = ∅
14 12 13 eqtrdi ( ¬ 𝐴 ∈ V → ran { 𝐴 } = ∅ )
15 14 unieqd ( ¬ 𝐴 ∈ V → ran { 𝐴 } = ∅ )
16 uni0 ∅ = ∅
17 15 16 eqtrdi ( ¬ 𝐴 ∈ V → ran { 𝐴 } = ∅ )
18 9 17 eqtr4d ( ¬ 𝐴 ∈ V → ( 2nd𝐴 ) = ran { 𝐴 } )
19 8 18 pm2.61i ( 2nd𝐴 ) = ran { 𝐴 }