Metamath Proof Explorer

Theorem cotrtrclfv

Description: The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020)

		Ref	Expression
	Assertion	cotrtrclfv	$⊢ (R \in V \land R \circ R \subseteq R) \to t+ (R) = R$

Proof

Step	Hyp	Ref	Expression
1		trclfv	$⊢ R \in V \to t+ (R) = ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
2	1	adantr	$⊢ (R \in V \land R \circ R \subseteq R) \to t+ (R) = ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
3		simpr	$⊢ (R \in V \land R \circ R \subseteq R) \to R \circ R \subseteq R$
4		ssid	$⊢ R \subseteq R$
5	3 4	jctil	$⊢ (R \in V \land R \circ R \subseteq R) \to (R \subseteq R \land R \circ R \subseteq R)$
6		trcleq2lem	$⊢ r = R \to ((R \subseteq r \land r \circ r \subseteq r) \leftrightarrow (R \subseteq R \land R \circ R \subseteq R))$
7	6	elabg	$⊢ R \in V \to (R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \leftrightarrow (R \subseteq R \land R \circ R \subseteq R))$
8	7	adantr	$⊢ (R \in V \land R \circ R \subseteq R) \to (R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \leftrightarrow (R \subseteq R \land R \circ R \subseteq R))$
9	5 8	mpbird	$⊢ (R \in V \land R \circ R \subseteq R) \to R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
10		intss1	$⊢ R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq R$
11	9 10	syl	$⊢ (R \in V \land R \circ R \subseteq R) \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq R$
12	2 11	eqsstrd	$⊢ (R \in V \land R \circ R \subseteq R) \to t+ (R) \subseteq R$
13		trclfvlb	$⊢ R \in V \to R \subseteq t+ (R)$
14	13	adantr	$⊢ (R \in V \land R \circ R \subseteq R) \to R \subseteq t+ (R)$
15	12 14	eqssd	$⊢ (R \in V \land R \circ R \subseteq R) \to t+ (R) = R$