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