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 \cap (A \times B)) = A \leftrightarrow \forall x \in A \exists y \in B x C y$

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$⊢ dom (C \cap (A \times B)) = ran {(C \cap (A \times B))}^{-1}$
2		cnvin	$⊢ {(C \cap (A \times B))}^{-1} = C^{-1} \cap {(A \times B)}^{-1}$
3		cnvxp	$⊢ {(A \times B)}^{-1} = B \times A$
4	3	ineq2i	$⊢ C^{-1} \cap {(A \times B)}^{-1} = C^{-1} \cap (B \times A)$
5	2 4	eqtri	$⊢ {(C \cap (A \times B))}^{-1} = C^{-1} \cap (B \times A)$
6	5	rneqi	$⊢ ran {(C \cap (A \times B))}^{-1} = ran (C^{-1} \cap (B \times A))$
7	1 6	eqtri	$⊢ dom (C \cap (A \times B)) = ran (C^{-1} \cap (B \times A))$
8	7	eqeq1i	$⊢ dom (C \cap (A \times B)) = A \leftrightarrow ran (C^{-1} \cap (B \times A)) = A$
9		rninxp	$⊢ ran (C^{-1} \cap (B \times A)) = A \leftrightarrow \forall x \in A \exists y \in B y C^{-1} x$
10		vex	$⊢ y \in V$
11		vex	$⊢ x \in V$
12	10 11	brcnv	$⊢ y C^{-1} x \leftrightarrow x C y$
13	12	rexbii	$⊢ \exists y \in B y C^{-1} x \leftrightarrow \exists y \in B x C y$
14	13	ralbii	$⊢ \forall x \in A \exists y \in B y C^{-1} x \leftrightarrow \forall x \in A \exists y \in B x C y$
15	8 9 14	3bitri	$⊢ dom (C \cap (A \times B)) = A \leftrightarrow \forall x \in A \exists y \in B x C y$