brtrclfv

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

		Ref	Expression
	Assertion	brtrclfv	$⊢ R \in V \to (A t+ (R) B \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to A r B))$

Step	Hyp	Ref	Expression
1		trclfv	$⊢ R \in V \to t+ (R) = ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
2	1	breqd	$⊢ R \in V \to (A t+ (R) B \leftrightarrow A ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} B)$
3		brintclab	$⊢ A ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} B \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to ⟨A, B⟩ \in r)$
4		df-br	$⊢ A r B \leftrightarrow ⟨A, B⟩ \in r$
5	4	imbi2i	$⊢ ((R \subseteq r \land r \circ r \subseteq r) \to A r B) \leftrightarrow ((R \subseteq r \land r \circ r \subseteq r) \to ⟨A, B⟩ \in r)$
6	5	albii	$⊢ \forall r ((R \subseteq r \land r \circ r \subseteq r) \to A r B) \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to ⟨A, B⟩ \in r)$
7	3 6	bitr4i	$⊢ A ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} B \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to A r B)$
8	2 7	bitrdi	$⊢ R \in V \to (A t+ (R) B \leftrightarrow \forall r ((R \subseteq r \land r \circ r \subseteq r) \to A r B))$

Metamath Proof Explorer