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

Metamath Proof Explorer

Theorem f1opr

Description: Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010)

Ref Expression
Assertion f1opr 
|- ( F : ( A X. B ) -1-1-> C <-> ( F : ( A X. B ) --> C /\ A. r e. A A. s e. B A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) ) )

Proof

Step Hyp Ref Expression
1 dff13 
 |-  ( F : ( A X. B ) -1-1-> C <-> ( F : ( A X. B ) --> C /\ A. v e. ( A X. B ) A. w e. ( A X. B ) ( ( F ` v ) = ( F ` w ) -> v = w ) ) )
2 fveq2 
 |-  ( v = <. r , s >. -> ( F ` v ) = ( F ` <. r , s >. ) )
3 df-ov 
 |-  ( r F s ) = ( F ` <. r , s >. )
4 2 3 eqtr4di 
 |-  ( v = <. r , s >. -> ( F ` v ) = ( r F s ) )
5 4 eqeq1d 
 |-  ( v = <. r , s >. -> ( ( F ` v ) = ( F ` w ) <-> ( r F s ) = ( F ` w ) ) )
6 eqeq1 
 |-  ( v = <. r , s >. -> ( v = w <-> <. r , s >. = w ) )
7 5 6 imbi12d 
 |-  ( v = <. r , s >. -> ( ( ( F ` v ) = ( F ` w ) -> v = w ) <-> ( ( r F s ) = ( F ` w ) -> <. r , s >. = w ) ) )
8 7 ralbidv 
 |-  ( v = <. r , s >. -> ( A. w e. ( A X. B ) ( ( F ` v ) = ( F ` w ) -> v = w ) <-> A. w e. ( A X. B ) ( ( r F s ) = ( F ` w ) -> <. r , s >. = w ) ) )
9 8 ralxp 
 |-  ( A. v e. ( A X. B ) A. w e. ( A X. B ) ( ( F ` v ) = ( F ` w ) -> v = w ) <-> A. r e. A A. s e. B A. w e. ( A X. B ) ( ( r F s ) = ( F ` w ) -> <. r , s >. = w ) )
10 fveq2 
 |-  ( w = <. t , u >. -> ( F ` w ) = ( F ` <. t , u >. ) )
11 df-ov 
 |-  ( t F u ) = ( F ` <. t , u >. )
12 10 11 eqtr4di 
 |-  ( w = <. t , u >. -> ( F ` w ) = ( t F u ) )
13 12 eqeq2d 
 |-  ( w = <. t , u >. -> ( ( r F s ) = ( F ` w ) <-> ( r F s ) = ( t F u ) ) )
14 eqeq2 
 |-  ( w = <. t , u >. -> ( <. r , s >. = w <-> <. r , s >. = <. t , u >. ) )
15 vex 
 |-  r e. _V
16 vex 
 |-  s e. _V
17 15 16 opth 
 |-  ( <. r , s >. = <. t , u >. <-> ( r = t /\ s = u ) )
18 14 17 bitrdi 
 |-  ( w = <. t , u >. -> ( <. r , s >. = w <-> ( r = t /\ s = u ) ) )
19 13 18 imbi12d 
 |-  ( w = <. t , u >. -> ( ( ( r F s ) = ( F ` w ) -> <. r , s >. = w ) <-> ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) ) )
20 19 ralxp 
 |-  ( A. w e. ( A X. B ) ( ( r F s ) = ( F ` w ) -> <. r , s >. = w ) <-> A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) )
21 20 2ralbii 
 |-  ( A. r e. A A. s e. B A. w e. ( A X. B ) ( ( r F s ) = ( F ` w ) -> <. r , s >. = w ) <-> A. r e. A A. s e. B A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) )
22 9 21 bitri 
 |-  ( A. v e. ( A X. B ) A. w e. ( A X. B ) ( ( F ` v ) = ( F ` w ) -> v = w ) <-> A. r e. A A. s e. B A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) )
23 22 anbi2i 
 |-  ( ( F : ( A X. B ) --> C /\ A. v e. ( A X. B ) A. w e. ( A X. B ) ( ( F ` v ) = ( F ` w ) -> v = w ) ) <-> ( F : ( A X. B ) --> C /\ A. r e. A A. s e. B A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) ) )
24 1 23 bitri 
 |-  ( F : ( A X. B ) -1-1-> C <-> ( F : ( A X. B ) --> C /\ A. r e. A A. s e. B A. t e. A A. u e. B ( ( r F s ) = ( t F u ) -> ( r = t /\ s = u ) ) ) )