Metamath Proof Explorer

Theorem trclubgi

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

		Ref	Expression
	Hypothesis	trclubgi.rex	$⊢ R \in V$
	Assertion	trclubgi	$⊢ ⋂ \{s \| (R \subseteq s \land s \circ s \subseteq s)\} \subseteq R \cup (dom R \times ran R)$

Proof

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