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 { 𝐴 }