# Metamath Proof Explorer

## Theorem trclubgNEW

Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020)

Ref Expression
Hypothesis trclubgNEW.rex ${⊢}{\phi }\to {R}\in \mathrm{V}$
Assertion trclubgNEW ${⊢}{\phi }\to \bigcap \left\{{x}|\left({R}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$

### Proof

Step Hyp Ref Expression
1 trclubgNEW.rex ${⊢}{\phi }\to {R}\in \mathrm{V}$
2 1 dmexd ${⊢}{\phi }\to \mathrm{dom}{R}\in \mathrm{V}$
3 rnexg ${⊢}{R}\in \mathrm{V}\to \mathrm{ran}{R}\in \mathrm{V}$
4 1 3 syl ${⊢}{\phi }\to \mathrm{ran}{R}\in \mathrm{V}$
5 2 4 xpexd ${⊢}{\phi }\to \mathrm{dom}{R}×\mathrm{ran}{R}\in \mathrm{V}$
6 unexg ${⊢}\left({R}\in \mathrm{V}\wedge \mathrm{dom}{R}×\mathrm{ran}{R}\in \mathrm{V}\right)\to {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\in \mathrm{V}$
7 1 5 6 syl2anc ${⊢}{\phi }\to {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\in \mathrm{V}$
8 id ${⊢}{x}={R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\to {x}={R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
9 8 8 coeq12d ${⊢}{x}={R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\to {x}\circ {x}=\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)$
10 9 8 sseq12d ${⊢}{x}={R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\to \left({x}\circ {x}\subseteq {x}↔\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)$
11 ssun1 ${⊢}{R}\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
12 11 a1i ${⊢}{\phi }\to {R}\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
13 cnvssrndm ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}$
14 coundi ${⊢}\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)=\left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}\right)\cup \left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)$
15 cnvss ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to {{{R}}^{-1}}^{-1}\subseteq {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}$
16 coss2 ${⊢}{{{R}}^{-1}}^{-1}\subseteq {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}\to \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {{{R}}^{-1}}^{-1}\subseteq \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}$
17 15 16 syl ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {{{R}}^{-1}}^{-1}\subseteq \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}$
18 cocnvcnv2 ${⊢}\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {{{R}}^{-1}}^{-1}=\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}$
19 cnvxp ${⊢}{\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}=\mathrm{dom}{R}×\mathrm{ran}{R}$
20 19 coeq2i ${⊢}\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}=\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
21 17 18 20 3sstr3g ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}\subseteq \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
22 ssequn1 ${⊢}\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}\subseteq \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)↔\left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}\right)\cup \left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)=\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
23 21 22 sylib ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}\right)\cup \left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)=\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
24 coundir ${⊢}\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)=\left({R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\cup \left(\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)$
25 coss1 ${⊢}{{{R}}^{-1}}^{-1}\subseteq {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}\to {{{R}}^{-1}}^{-1}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
26 15 25 syl ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to {{{R}}^{-1}}^{-1}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
27 cocnvcnv1 ${⊢}{{{R}}^{-1}}^{-1}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)={R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
28 19 coeq1i ${⊢}{\left(\mathrm{ran}{R}×\mathrm{dom}{R}\right)}^{-1}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)=\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
29 26 27 28 3sstr3g ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to {R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
30 ssequn1 ${⊢}{R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)↔\left({R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\cup \left(\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)=\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
31 29 30 sylib ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left({R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\cup \left(\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)=\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
32 xptrrel ${⊢}\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq \mathrm{dom}{R}×\mathrm{ran}{R}$
33 ssun2 ${⊢}\mathrm{dom}{R}×\mathrm{ran}{R}\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
34 32 33 sstri ${⊢}\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
35 34 a1i ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
36 31 35 eqsstrd ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left({R}\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\cup \left(\left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
37 24 36 eqsstrid ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
38 23 37 eqsstrd ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ {R}\right)\cup \left(\left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
39 14 38 eqsstrid ${⊢}{{R}}^{-1}\subseteq \mathrm{ran}{R}×\mathrm{dom}{R}\to \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
40 13 39 mp1i ${⊢}{\phi }\to \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\circ \left({R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)\right)\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$
41 7 10 12 40 clublem ${⊢}{\phi }\to \bigcap \left\{{x}|\left({R}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\subseteq {R}\cup \left(\mathrm{dom}{R}×\mathrm{ran}{R}\right)$