Metamath Proof Explorer

Theorem trclubi

Description: The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020) (Revised by RP, 28-Apr-2020) (Revised by AV, 26-Mar-2021)

		Ref	Expression
	Hypotheses	trclubi.rel	$⊢ Rel R$
		trclubi.rex	$⊢ R \in V$
	Assertion	trclubi	$⊢ ⋂ \{s \| (R \subseteq s \land s \circ s \subseteq s)\} \subseteq dom R \times ran R$

Proof

Step	Hyp	Ref	Expression
1		trclubi.rel	$⊢ Rel R$
2		trclubi.rex	$⊢ R \in V$
3		relssdmrn	$⊢ Rel R \to R \subseteq dom R \times ran R$
4		ssequn1	$⊢ R \subseteq dom R \times ran R \leftrightarrow R \cup (dom R \times ran R) = dom R \times ran R$
5	3 4	sylib	$⊢ Rel R \to R \cup (dom R \times ran R) = dom R \times ran R$
6	1 5	ax-mp	$⊢ R \cup (dom R \times ran R) = dom R \times ran R$
7		trclublem	$⊢ R \in V \to R \cup (dom R \times ran R) \in \{s \| (R \subseteq s \land s \circ s \subseteq s)\}$
8	2 7	ax-mp	$⊢ R \cup (dom R \times ran R) \in \{s \| (R \subseteq s \land s \circ s \subseteq s)\}$
9	6 8	eqeltrri	$⊢ dom R \times ran R \in \{s \| (R \subseteq s \land s \circ s \subseteq s)\}$
10		intss1	$⊢ dom R \times ran R \in \{s \| (R \subseteq s \land s \circ s \subseteq s)\} \to ⋂ \{s \| (R \subseteq s \land s \circ s \subseteq s)\} \subseteq dom R \times ran R$
11	9 10	ax-mp	$⊢ ⋂ \{s \| (R \subseteq s \land s \circ s \subseteq s)\} \subseteq dom R \times ran R$