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 )