brcnvtrclfv

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

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

Step	Hyp	Ref	Expression
1		brcnvg	$⊢ (A \in V \land B \in W) \to (A {t+ (R)}^{-1} B \leftrightarrow B t+ (R) A)$
2	1	3adant1	$⊢ (R \in U \land A \in V \land B \in W) \to (A {t+ (R)}^{-1} B \leftrightarrow B t+ (R) A)$
3		brtrclfv	$⊢ R \in U \to (B t+ (R) A \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to B r A))$
4	3	3ad2ant1	$⊢ (R \in U \land A \in V \land B \in W) \to (B t+ (R) A \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to B r A))$
5	2 4	bitrd	$⊢ (R \in U \land A \in V \land B \in W) \to (A {t+ (R)}^{-1} B \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to B r A))$

Metamath Proof Explorer