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

Metamath Proof Explorer

Theorem fprg

Description: A function with a domain of two elements. (Contributed by FL, 2-Feb-2014)

Ref Expression
Assertion fprg 
|- ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. E -> A e. _V )
2 elex 
 |-  ( B e. F -> B e. _V )
3 1 2 anim12i 
 |-  ( ( A e. E /\ B e. F ) -> ( A e. _V /\ B e. _V ) )
4 elex 
 |-  ( C e. G -> C e. _V )
5 elex 
 |-  ( D e. H -> D e. _V )
6 4 5 anim12i 
 |-  ( ( C e. G /\ D e. H ) -> ( C e. _V /\ D e. _V ) )
7 neeq1 
 |-  ( A = if ( A e. _V , A , (/) ) -> ( A =/= B <-> if ( A e. _V , A , (/) ) =/= B ) )
8 opeq1 
 |-  ( A = if ( A e. _V , A , (/) ) -> <. A , C >. = <. if ( A e. _V , A , (/) ) , C >. )
9 8 preq1d 
 |-  ( A = if ( A e. _V , A , (/) ) -> { <. A , C >. , <. B , D >. } = { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } )
10 preq1 
 |-  ( A = if ( A e. _V , A , (/) ) -> { A , B } = { if ( A e. _V , A , (/) ) , B } )
11 9 10 feq12d 
 |-  ( A = if ( A e. _V , A , (/) ) -> ( { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) )
12 7 11 imbi12d 
 |-  ( A = if ( A e. _V , A , (/) ) -> ( ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= B -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) ) )
13 neeq2 
 |-  ( B = if ( B e. _V , B , (/) ) -> ( if ( A e. _V , A , (/) ) =/= B <-> if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) ) )
14 opeq1 
 |-  ( B = if ( B e. _V , B , (/) ) -> <. B , D >. = <. if ( B e. _V , B , (/) ) , D >. )
15 14 preq2d 
 |-  ( B = if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } = { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } )
16 preq2 
 |-  ( B = if ( B e. _V , B , (/) ) -> { if ( A e. _V , A , (/) ) , B } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
17 15 16 feq12d 
 |-  ( B = if ( B e. _V , B , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) )
18 13 17 imbi12d 
 |-  ( B = if ( B e. _V , B , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= B -> { <. if ( A e. _V , A , (/) ) , C >. , <. B , D >. } : { if ( A e. _V , A , (/) ) , B } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) ) )
19 opeq2 
 |-  ( C = if ( C e. _V , C , (/) ) -> <. if ( A e. _V , A , (/) ) , C >. = <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. )
20 19 preq1d 
 |-  ( C = if ( C e. _V , C , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } = { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } )
21 eqidd 
 |-  ( C = if ( C e. _V , C , (/) ) -> { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
22 preq1 
 |-  ( C = if ( C e. _V , C , (/) ) -> { C , D } = { if ( C e. _V , C , (/) ) , D } )
23 20 21 22 feq123d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } <-> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) )
24 23 imbi2d 
 |-  ( C = if ( C e. _V , C , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , C >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { C , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) ) )
25 opeq2 
 |-  ( D = if ( D e. _V , D , (/) ) -> <. if ( B e. _V , B , (/) ) , D >. = <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. )
26 25 preq2d 
 |-  ( D = if ( D e. _V , D , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } = { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } )
27 eqidd 
 |-  ( D = if ( D e. _V , D , (/) ) -> { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } = { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } )
28 preq2 
 |-  ( D = if ( D e. _V , D , (/) ) -> { if ( C e. _V , C , (/) ) , D } = { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } )
29 26 27 28 feq123d 
 |-  ( D = if ( D e. _V , D , (/) ) -> ( { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } <-> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } ) )
30 29 imbi2d 
 |-  ( D = if ( D e. _V , D , (/) ) -> ( ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , D >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , D } ) <-> ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } ) ) )
31 0ex 
 |-  (/) e. _V
32 31 elimel 
 |-  if ( A e. _V , A , (/) ) e. _V
33 31 elimel 
 |-  if ( B e. _V , B , (/) ) e. _V
34 31 elimel 
 |-  if ( C e. _V , C , (/) ) e. _V
35 31 elimel 
 |-  if ( D e. _V , D , (/) ) e. _V
36 32 33 34 35 fpr 
 |-  ( if ( A e. _V , A , (/) ) =/= if ( B e. _V , B , (/) ) -> { <. if ( A e. _V , A , (/) ) , if ( C e. _V , C , (/) ) >. , <. if ( B e. _V , B , (/) ) , if ( D e. _V , D , (/) ) >. } : { if ( A e. _V , A , (/) ) , if ( B e. _V , B , (/) ) } --> { if ( C e. _V , C , (/) ) , if ( D e. _V , D , (/) ) } )
37 12 18 24 30 36 dedth4h 
 |-  ( ( ( A e. _V /\ B e. _V ) /\ ( C e. _V /\ D e. _V ) ) -> ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) )
38 3 6 37 syl2an 
 |-  ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) ) -> ( A =/= B -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } ) )
39 38 3impia 
 |-  ( ( ( A e. E /\ B e. F ) /\ ( C e. G /\ D e. H ) /\ A =/= B ) -> { <. A , C >. , <. B , D >. } : { A , B } --> { C , D } )