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 } )