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 
|- ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } )

Proof

Step Hyp Ref Expression
1 rneq 
 |-  ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = ran { <. 2 , 6 >. , <. 3 , 9 >. } )
2 df-pr 
 |-  { <. 2 , 6 >. , <. 3 , 9 >. } = ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } )
3 2 rneqi 
 |-  ran { <. 2 , 6 >. , <. 3 , 9 >. } = ran ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } )
4 rnun 
 |-  ran ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } ) = ( ran { <. 2 , 6 >. } u. ran { <. 3 , 9 >. } )
5 2nn 
 |-  2 e. NN
6 5 elexi 
 |-  2 e. _V
7 6 rnsnop 
 |-  ran { <. 2 , 6 >. } = { 6 }
8 3nn 
 |-  3 e. NN
9 8 elexi 
 |-  3 e. _V
10 9 rnsnop 
 |-  ran { <. 3 , 9 >. } = { 9 }
11 7 10 uneq12i 
 |-  ( ran { <. 2 , 6 >. } u. ran { <. 3 , 9 >. } ) = ( { 6 } u. { 9 } )
12 df-pr 
 |-  { 6 , 9 } = ( { 6 } u. { 9 } )
13 11 12 eqtr4i 
 |-  ( ran { <. 2 , 6 >. } u. ran { <. 3 , 9 >. } ) = { 6 , 9 }
14 3 4 13 3eqtri 
 |-  ran { <. 2 , 6 >. , <. 3 , 9 >. } = { 6 , 9 }
15 1 14 eqtrdi 
 |-  ( F = { <. 2 , 6 >. , <. 3 , 9 >. } -> ran F = { 6 , 9 } )