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

Metamath Proof Explorer

Theorem dminxp

Description: Two ways to express totality of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 dfdm4 
 |-  dom ( C i^i ( A X. B ) ) = ran `' ( C i^i ( A X. B ) )
2 cnvin 
 |-  `' ( C i^i ( A X. B ) ) = ( `' C i^i `' ( A X. B ) )
3 cnvxp 
 |-  `' ( A X. B ) = ( B X. A )
4 3 ineq2i 
 |-  ( `' C i^i `' ( A X. B ) ) = ( `' C i^i ( B X. A ) )
5 2 4 eqtri 
 |-  `' ( C i^i ( A X. B ) ) = ( `' C i^i ( B X. A ) )
6 5 rneqi 
 |-  ran `' ( C i^i ( A X. B ) ) = ran ( `' C i^i ( B X. A ) )
7 1 6 eqtri 
 |-  dom ( C i^i ( A X. B ) ) = ran ( `' C i^i ( B X. A ) )
8 7 eqeq1i 
 |-  ( dom ( C i^i ( A X. B ) ) = A <-> ran ( `' C i^i ( B X. A ) ) = A )
9 rninxp 
 |-  ( ran ( `' C i^i ( B X. A ) ) = A <-> A. x e. A E. y e. B y `' C x )
10 vex 
 |-  y e. _V
11 vex 
 |-  x e. _V
12 10 11 brcnv 
 |-  ( y `' C x <-> x C y )
13 12 rexbii 
 |-  ( E. y e. B y `' C x <-> E. y e. B x C y )
14 13 ralbii 
 |-  ( A. x e. A E. y e. B y `' C x <-> A. x e. A E. y e. B x C y )
15 8 9 14 3bitri 
 |-  ( dom ( C i^i ( A X. B ) ) = A <-> A. x e. A E. y e. B x C y )