brcodir

Description: Two ways of saying that two elements have an upper bound. (Contributed by Mario Carneiro, 3-Nov-2015)

		Ref	Expression
	Assertion	brcodir	$⊢ (A \in V \land B \in W) \to (A (R^{-1} \circ R) B \leftrightarrow \exists z (A R z \land B R z))$

Step	Hyp	Ref	Expression
1		brcog	$⊢ (A \in V \land B \in W) \to (A (R^{-1} \circ R) B \leftrightarrow \exists z (A R z \land z R^{-1} B))$
2		vex	$⊢ z \in V$
3		brcnvg	$⊢ (z \in V \land B \in W) \to (z R^{-1} B \leftrightarrow B R z)$
4	2 3	mpan	$⊢ B \in W \to (z R^{-1} B \leftrightarrow B R z)$
5	4	anbi2d	$⊢ B \in W \to ((A R z \land z R^{-1} B) \leftrightarrow (A R z \land B R z))$
6	5	adantl	$⊢ (A \in V \land B \in W) \to ((A R z \land z R^{-1} B) \leftrightarrow (A R z \land B R z))$
7	6	exbidv	$⊢ (A \in V \land B \in W) \to (\exists z (A R z \land z R^{-1} B) \leftrightarrow \exists z (A R z \land B R z))$
8	1 7	bitrd	$⊢ (A \in V \land B \in W) \to (A (R^{-1} \circ R) B \leftrightarrow \exists z (A R z \land B R z))$

Metamath Proof Explorer