rntrcl

Description: The range of the transitive closure is equal to the range of its base relation. (Contributed by RP, 1-Nov-2020)

		Ref	Expression
	Assertion	rntrcl	$⊢ X \in V \to ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} = ran X$

Step	Hyp	Ref	Expression
1		trclubg	$⊢ X \in V \to ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq X \cup (dom X \times ran X)$
2		rnss	$⊢ ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq X \cup (dom X \times ran X) \to ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq ran (X \cup (dom X \times ran X))$
3	1 2	syl	$⊢ X \in V \to ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq ran (X \cup (dom X \times ran X))$
4		rnun	$⊢ ran (X \cup (dom X \times ran X)) = ran X \cup ran (dom X \times ran X)$
5		rnxpss	$⊢ ran (dom X \times ran X) \subseteq ran X$
6		ssequn2	$⊢ ran (dom X \times ran X) \subseteq ran X \leftrightarrow ran X \cup ran (dom X \times ran X) = ran X$
7	5 6	mpbi	$⊢ ran X \cup ran (dom X \times ran X) = ran X$
8	4 7	eqtri	$⊢ ran (X \cup (dom X \times ran X)) = ran X$
9	3 8	sseqtrdi	$⊢ X \in V \to ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \subseteq ran X$
10		ssmin	$⊢ X \subseteq ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}$
11		rnss	$⊢ X \subseteq ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} \to ran X \subseteq ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}$
12	10 11	mp1i	$⊢ X \in V \to ran X \subseteq ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\}$
13	9 12	eqssd	$⊢ X \in V \to ran ⋂ \{x \| (X \subseteq x \land x \circ x \subseteq x)\} = ran X$

Metamath Proof Explorer