trclfvss

Description: The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020)

		Ref	Expression
	Assertion	trclfvss	$⊢ (R \in V \land S \in W \land R \subseteq S) \to t+ (R) \subseteq t+ (S)$

Step	Hyp	Ref	Expression
1		trclsslem	$⊢ R \subseteq S \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq ⋂ \{r \| (S \subseteq r \land r \circ r \subseteq r)\}$
2	1	3ad2ant3	$⊢ (R \in V \land S \in W \land R \subseteq S) \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq ⋂ \{r \| (S \subseteq r \land r \circ r \subseteq r)\}$
3		trclfv	$⊢ R \in V \to t+ (R) = ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
4	3	3ad2ant1	$⊢ (R \in V \land S \in W \land R \subseteq S) \to t+ (R) = ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
5		trclfv	$⊢ S \in W \to t+ (S) = ⋂ \{r \| (S \subseteq r \land r \circ r \subseteq r)\}$
6	5	3ad2ant2	$⊢ (R \in V \land S \in W \land R \subseteq S) \to t+ (S) = ⋂ \{r \| (S \subseteq r \land r \circ r \subseteq r)\}$
7	2 4 6	3sstr4d	$⊢ (R \in V \land S \in W \land R \subseteq S) \to t+ (R) \subseteq t+ (S)$

Metamath Proof Explorer