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

Metamath Proof Explorer

Theorem ex-rn

Description: Example for df-rn . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-rn ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ran 𝐹 = { 6 , 9 } )

Proof

Step Hyp Ref Expression
1 rneq ⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ran 𝐹 = ran { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } )
2 df-pr ⊢ { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } )
3 2 rneqi ⊢ ran { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = ran ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } )
4 rnun ⊢ ran ( { ⟨ 2 , 6 ⟩ } ∪ { ⟨ 3 , 9 ⟩ } ) = ( ran { ⟨ 2 , 6 ⟩ } ∪ ran { ⟨ 3 , 9 ⟩ } )
5 2nn ⊢ 2 ∈ ℕ
6 5 elexi ⊢ 2 ∈ V
7 6 rnsnop ⊢ ran { ⟨ 2 , 6 ⟩ } = { 6 }
8 3nn ⊢ 3 ∈ ℕ
9 8 elexi ⊢ 3 ∈ V
10 9 rnsnop ⊢ ran { ⟨ 3 , 9 ⟩ } = { 9 }
11 7 10 uneq12i ⊢ ( ran { ⟨ 2 , 6 ⟩ } ∪ ran { ⟨ 3 , 9 ⟩ } ) = ( { 6 } ∪ { 9 } )
12 df-pr ⊢ { 6 , 9 } = ( { 6 } ∪ { 9 } )
13 11 12 eqtr4i ⊢ ( ran { ⟨ 2 , 6 ⟩ } ∪ ran { ⟨ 3 , 9 ⟩ } ) = { 6 , 9 }
14 3 4 13 3eqtri ⊢ ran { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } = { 6 , 9 }
15 1 14 eqtrdi ⊢ ( 𝐹 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ran 𝐹 = { 6 , 9 } )