Metamath Proof Explorer

Theorem trclub

Description: The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 17-May-2020)

		Ref	Expression
	Assertion	trclub	$⊢ (R \in V \land Rel R) \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq dom R \times ran R$

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	$⊢ Rel R \to R \subseteq dom R \times ran R$
2		ssequn1	$⊢ R \subseteq dom R \times ran R \leftrightarrow R \cup (dom R \times ran R) = dom R \times ran R$
3	1 2	sylib	$⊢ Rel R \to R \cup (dom R \times ran R) = dom R \times ran R$
4		trclublem	$⊢ R \in V \to R \cup (dom R \times ran R) \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
5		eleq1	$⊢ R \cup (dom R \times ran R) = dom R \times ran R \to (R \cup (dom R \times ran R) \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \leftrightarrow dom R \times ran R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\})$
6	5	biimpa	$⊢ (R \cup (dom R \times ran R) = dom R \times ran R \land R \cup (dom R \times ran R) \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\}) \to dom R \times ran R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
7	3 4 6	syl2anr	$⊢ (R \in V \land Rel R) \to dom R \times ran R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
8		intss1	$⊢ dom R \times ran R \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq dom R \times ran R$
9	7 8	syl	$⊢ (R \in V \land Rel R) \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq dom R \times ran R$