# Metamath Proof Explorer

## Theorem 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 \mathrm{ran}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}=\mathrm{ran}{X}$

### Proof

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