Metamath Proof Explorer

Theorem trclubg

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

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

Proof

Step	Hyp	Ref	Expression
1		trclublem	$⊢ R \in V \to R \cup (dom R \times ran R) \in \{r \| (R \subseteq r \land r \circ r \subseteq r)\}$
2		intss1	$⊢ R \cup (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 R \cup (dom R \times ran R)$
3	1 2	syl	$⊢ R \in V \to ⋂ \{r \| (R \subseteq r \land r \circ r \subseteq r)\} \subseteq R \cup (dom R \times ran R)$