# Metamath Proof Explorer

## Theorem dmtrcl

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

Ref Expression
Assertion dmtrcl ${⊢}{X}\in {V}\to \mathrm{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}=\mathrm{dom}{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 dmss ${⊢}\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{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\subseteq \mathrm{dom}\left({X}\cup \left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)\right)$
3 1 2 syl ${⊢}{X}\in {V}\to \mathrm{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\subseteq \mathrm{dom}\left({X}\cup \left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)\right)$
4 dmun ${⊢}\mathrm{dom}\left({X}\cup \left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)\right)=\mathrm{dom}{X}\cup \mathrm{dom}\left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)$
5 dmxpss ${⊢}\mathrm{dom}\left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)\subseteq \mathrm{dom}{X}$
6 ssequn2 ${⊢}\mathrm{dom}\left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)\subseteq \mathrm{dom}{X}↔\mathrm{dom}{X}\cup \mathrm{dom}\left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)=\mathrm{dom}{X}$
7 5 6 mpbi ${⊢}\mathrm{dom}{X}\cup \mathrm{dom}\left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)=\mathrm{dom}{X}$
8 4 7 eqtri ${⊢}\mathrm{dom}\left({X}\cup \left(\mathrm{dom}{X}×\mathrm{ran}{X}\right)\right)=\mathrm{dom}{X}$
9 3 8 sseqtrdi ${⊢}{X}\in {V}\to \mathrm{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\subseteq \mathrm{dom}{X}$
10 ssmin ${⊢}{X}\subseteq \bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}$
11 dmss ${⊢}{X}\subseteq \bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\to \mathrm{dom}{X}\subseteq \mathrm{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}$
12 10 11 mp1i ${⊢}{X}\in {V}\to \mathrm{dom}{X}\subseteq \mathrm{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}$
13 9 12 eqssd ${⊢}{X}\in {V}\to \mathrm{dom}\bigcap \left\{{x}|\left({X}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}=\mathrm{dom}{X}$