rntrclfvOAI

Description: The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020)

		Ref	Expression
	Assertion	rntrclfvOAI	$⊢ R \in V \to ran t+ (R) = ran R$

Step	Hyp	Ref	Expression
1		trclfvub	$⊢ R \in V \to t+ (R) \subseteq R \cup (dom R \times ran R)$
2		rnss	$⊢ t+ (R) \subseteq R \cup (dom R \times ran R) \to ran t+ (R) \subseteq ran (R \cup (dom R \times ran R))$
3	1 2	syl	$⊢ R \in V \to ran t+ (R) \subseteq ran (R \cup (dom R \times ran R))$
4		rnun	$⊢ ran (R \cup (dom R \times ran R)) = ran R \cup ran (dom R \times ran R)$
5	4	a1i	$⊢ R \in V \to ran (R \cup (dom R \times ran R)) = ran R \cup ran (dom R \times ran R)$
6		rnxpss	$⊢ ran (dom R \times ran R) \subseteq ran R$
7		ssequn2	$⊢ ran (dom R \times ran R) \subseteq ran R \leftrightarrow ran R \cup ran (dom R \times ran R) = ran R$
8	6 7	mpbi	$⊢ ran R \cup ran (dom R \times ran R) = ran R$
9	5 8	eqtrdi	$⊢ R \in V \to ran (R \cup (dom R \times ran R)) = ran R$
10	3 9	sseqtrd	$⊢ R \in V \to ran t+ (R) \subseteq ran R$
11		trclfvlb	$⊢ R \in V \to R \subseteq t+ (R)$
12		rnss	$⊢ R \subseteq t+ (R) \to ran R \subseteq ran t+ (R)$
13	11 12	syl	$⊢ R \in V \to ran R \subseteq ran t+ (R)$
14	10 13	eqssd	$⊢ R \in V \to ran t+ (R) = ran R$

Metamath Proof Explorer