# Metamath Proof Explorer

## Theorem fpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypotheses fpr.1
`|- A e. _V`
fpr.2
`|- B e. _V`
fpr.3
`|- C e. _V`
fpr.4
`|- D e. _V`
Assertion fpr
`|- ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )`

### Proof

Step Hyp Ref Expression
1 fpr.1
` |-  A e. _V`
2 fpr.2
` |-  B e. _V`
3 fpr.3
` |-  C e. _V`
4 fpr.4
` |-  D e. _V`
5 1 2 3 4 funpr
` |-  ( A =/= B -> Fun { <. A , C >. , <. B , D >. } )`
6 3 4 dmprop
` |-  dom { <. A , C >. , <. B , D >. } = { A , B }`
7 df-fn
` |-  ( { <. A , C >. , <. B , D >. } Fn { A , B } <-> ( Fun { <. A , C >. , <. B , D >. } /\ dom { <. A , C >. , <. B , D >. } = { A , B } ) )`
8 5 6 7 sylanblrc
` |-  ( A =/= B -> { <. A , C >. , <. B , D >. } Fn { A , B } )`
9 df-pr
` |-  { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } )`
10 9 rneqi
` |-  ran { <. A , C >. , <. B , D >. } = ran ( { <. A , C >. } u. { <. B , D >. } )`
11 rnun
` |-  ran ( { <. A , C >. } u. { <. B , D >. } ) = ( ran { <. A , C >. } u. ran { <. B , D >. } )`
12 1 rnsnop
` |-  ran { <. A , C >. } = { C }`
13 2 rnsnop
` |-  ran { <. B , D >. } = { D }`
14 12 13 uneq12i
` |-  ( ran { <. A , C >. } u. ran { <. B , D >. } ) = ( { C } u. { D } )`
15 df-pr
` |-  { C , D } = ( { C } u. { D } )`
16 14 15 eqtr4i
` |-  ( ran { <. A , C >. } u. ran { <. B , D >. } ) = { C , D }`
17 10 11 16 3eqtri
` |-  ran { <. A , C >. , <. B , D >. } = { C , D }`
18 17 eqimssi
` |-  ran { <. A , C >. , <. B , D >. } C_ { C , D }`
19 df-f
` |-  ( { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } <-> ( { <. A , C >. , <. B , D >. } Fn { A , B } /\ ran { <. A , C >. , <. B , D >. } C_ { C , D } ) )`
20 8 18 19 sylanblrc
` |-  ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )`