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

Metamath Proof Explorer

Theorem foov

Description: An onto mapping of an operation expressed in terms of operation values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion foov 
|- ( F : ( A X. B ) -onto-> C <-> ( F : ( A X. B ) --> C /\ A. z e. C E. x e. A E. y e. B z = ( x F y ) ) )

Proof

Step Hyp Ref Expression
1 dffo3 
 |-  ( F : ( A X. B ) -onto-> C <-> ( F : ( A X. B ) --> C /\ A. z e. C E. w e. ( A X. B ) z = ( F ` w ) ) )
2 fveq2 
 |-  ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
3 df-ov 
 |-  ( x F y ) = ( F ` <. x , y >. )
4 2 3 eqtr4di 
 |-  ( w = <. x , y >. -> ( F ` w ) = ( x F y ) )
5 4 eqeq2d 
 |-  ( w = <. x , y >. -> ( z = ( F ` w ) <-> z = ( x F y ) ) )
6 5 rexxp 
 |-  ( E. w e. ( A X. B ) z = ( F ` w ) <-> E. x e. A E. y e. B z = ( x F y ) )
7 6 ralbii 
 |-  ( A. z e. C E. w e. ( A X. B ) z = ( F ` w ) <-> A. z e. C E. x e. A E. y e. B z = ( x F y ) )
8 7 anbi2i 
 |-  ( ( F : ( A X. B ) --> C /\ A. z e. C E. w e. ( A X. B ) z = ( F ` w ) ) <-> ( F : ( A X. B ) --> C /\ A. z e. C E. x e. A E. y e. B z = ( x F y ) ) )
9 1 8 bitri 
 |-  ( F : ( A X. B ) -onto-> C <-> ( F : ( A X. B ) --> C /\ A. z e. C E. x e. A E. y e. B z = ( x F y ) ) )