Metamath Proof Explorer

Theorem rninxp

Description: Two ways to express surjectivity of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion rninxp 
|- ( ran ( C i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x C y )

Proof

Step Hyp Ref Expression
1 dfss3 
 |-  ( B C_ ran ( C |` A ) <-> A. y e. B y e. ran ( C |` A ) )
2 ssrnres 
 |-  ( B C_ ran ( C |` A ) <-> ran ( C i^i ( A X. B ) ) = B )
3 df-ima 
 |-  ( C " A ) = ran ( C |` A )
4 3 eleq2i 
 |-  ( y e. ( C " A ) <-> y e. ran ( C |` A ) )
5 vex 
 |-  y e. _V
6 5 elima 
 |-  ( y e. ( C " A ) <-> E. x e. A x C y )
7 4 6 bitr3i 
 |-  ( y e. ran ( C |` A ) <-> E. x e. A x C y )
8 7 ralbii 
 |-  ( A. y e. B y e. ran ( C |` A ) <-> A. y e. B E. x e. A x C y )
9 1 2 8 3bitr3i 
 |-  ( ran ( C i^i ( A X. B ) ) = B <-> A. y e. B E. x e. A x C y )