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

Metamath Proof Explorer

Theorem rnpropg

Description: The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017)

Ref Expression
Assertion rnpropg ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐶 , 𝐷 } )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
2 1 rneqi ⊢ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
3 rnsnopg ⊢ ( 𝐴 ∈ 𝑉 → ran { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐶 } )
4 3 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐶 } )
5 rnsnopg ⊢ ( 𝐵 ∈ 𝑊 → ran { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐷 } )
6 5 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐷 } )
7 4 6 uneq12d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( { 𝐶 } ∪ { 𝐷 } ) )
8 rnun ⊢ ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } )
9 df-pr ⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
10 7 8 9 3eqtr4g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = { 𝐶 , 𝐷 } )
11 2 10 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐶 , 𝐷 } )