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

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 ⊢ 2 nd ⁡ A = ⋃ ran ⁡ A

Proof

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