codir

Description: Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013)

		Ref	Expression
	Assertion	codir	$⊢ A \times B \subseteq R^{-1} \circ R \leftrightarrow \forall x \in A \forall y \in B \exists z (x R z \land y R z)$

Step	Hyp	Ref	Expression
1		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
2		df-br	$⊢ x (R^{-1} \circ R) y \leftrightarrow ⟨x, y⟩ \in (R^{-1} \circ R)$
3		brcodir	$⊢ (x \in V \land y \in V) \to (x (R^{-1} \circ R) y \leftrightarrow \exists z (x R z \land y R z))$
4	3	el2v	$⊢ x (R^{-1} \circ R) y \leftrightarrow \exists z (x R z \land y R z)$
5	2 4	bitr3i	$⊢ ⟨x, y⟩ \in (R^{-1} \circ R) \leftrightarrow \exists z (x R z \land y R z)$
6	1 5	imbi12i	$⊢ (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R^{-1} \circ R)) \leftrightarrow ((x \in A \land y \in B) \to \exists z (x R z \land y R z))$
7	6	2albii	$⊢ \forall x \forall y (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R^{-1} \circ R)) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to \exists z (x R z \land y R z))$
8		relxp	$⊢ Rel (A \times B)$
9		ssrel	$⊢ Rel (A \times B) \to (A \times B \subseteq R^{-1} \circ R \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R^{-1} \circ R)))$
10	8 9	ax-mp	$⊢ A \times B \subseteq R^{-1} \circ R \leftrightarrow \forall x \forall y (⟨x, y⟩ \in (A \times B) \to ⟨x, y⟩ \in (R^{-1} \circ R))$
11		r2al	$⊢ \forall x \in A \forall y \in B \exists z (x R z \land y R z) \leftrightarrow \forall x \forall y ((x \in A \land y \in B) \to \exists z (x R z \land y R z))$
12	7 10 11	3bitr4i	$⊢ A \times B \subseteq R^{-1} \circ R \leftrightarrow \forall x \in A \forall y \in B \exists z (x R z \land y R z)$

Metamath Proof Explorer