reltrclfv

Description: The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020)

		Ref	Expression
	Assertion	reltrclfv	$⊢ (R \in V \land Rel R) \to Rel t+ (R)$

Step	Hyp	Ref	Expression
1		trclfvub	$⊢ R \in V \to t+ (R) \subseteq R \cup (dom R \times ran R)$
2	1	adantr	$⊢ (R \in V \land Rel R) \to t+ (R) \subseteq R \cup (dom R \times ran R)$
3		simpr	$⊢ (R \in V \land Rel R) \to Rel R$
4		relssdmrn	$⊢ Rel R \to R \subseteq dom R \times ran R$
5		ssequn1	$⊢ R \subseteq dom R \times ran R \leftrightarrow R \cup (dom R \times ran R) = dom R \times ran R$
6	5	biimpi	$⊢ R \subseteq dom R \times ran R \to R \cup (dom R \times ran R) = dom R \times ran R$
7	3 4 6	3syl	$⊢ (R \in V \land Rel R) \to R \cup (dom R \times ran R) = dom R \times ran R$
8	2 7	sseqtrd	$⊢ (R \in V \land Rel R) \to t+ (R) \subseteq dom R \times ran R$
9		xpss	$⊢ dom R \times ran R \subseteq V \times V$
10	8 9	sstrdi	$⊢ (R \in V \land Rel R) \to t+ (R) \subseteq V \times V$
11		df-rel	$⊢ Rel t+ (R) \leftrightarrow t+ (R) \subseteq V \times V$
12	10 11	sylibr	$⊢ (R \in V \land Rel R) \to Rel t+ (R)$

Metamath Proof Explorer