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