Metamath Proof Explorer

Theorem brcnvtrclfvcnv

Description: Two ways of expressing the transitive closure of the converse of the converse of a binary relation. (Contributed by RP, 10-May-2020)

		Ref	Expression
	Assertion	brcnvtrclfvcnv	$⊢ (R \in U \land A \in V \land B \in W) \to (A {t+ (R^{-1})}^{-1} B \leftrightarrow \forall r ((R^{-1} \subseteq r \land r \circ r \subseteq r) \to B r A))$

Step	Hyp	Ref	Expression
1		cnvexg	$⊢ R \in U \to R^{-1} \in V$
2		brcnvtrclfv	$⊢ (R^{-1} \in V \land A \in V \land B \in W) \to (A {t+ (R^{-1})}^{-1} B \leftrightarrow \forall r ((R^{-1} \subseteq r \land r \circ r \subseteq r) \to B r A))$
3	1 2	syl3an1	$⊢ (R \in U \land A \in V \land B \in W) \to (A {t+ (R^{-1})}^{-1} B \leftrightarrow \forall r ((R^{-1} \subseteq r \land r \circ r \subseteq r) \to B r A))$