Metamath Proof Explorer

Theorem trclexi

Description: The transitive closure of a set exists. (Contributed by RP, 27-Oct-2020)

Ref Expression
Hypothesis trclexi.1 ${⊢}{A}\in {V}$
Assertion trclexi ${⊢}\bigcap \left\{{x}|\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\in \mathrm{V}$

Proof

Step Hyp Ref Expression
1 trclexi.1 ${⊢}{A}\in {V}$
2 ssun1 ${⊢}{A}\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)$
3 coundir ${⊢}\left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)=\left({A}\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\right)\cup \left(\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\right)$
4 coundi ${⊢}{A}\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)=\left({A}\circ {A}\right)\cup \left({A}\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)$
5 cossxp ${⊢}{A}\circ {A}\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
6 cossxp ${⊢}{A}\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)×\mathrm{ran}{A}$
7 dmxpss ${⊢}\mathrm{dom}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}{A}$
8 xpss1 ${⊢}\mathrm{dom}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}{A}\to \mathrm{dom}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)×\mathrm{ran}{A}\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
9 7 8 ax-mp ${⊢}\mathrm{dom}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)×\mathrm{ran}{A}\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
10 6 9 sstri ${⊢}{A}\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
11 5 10 unssi ${⊢}\left({A}\circ {A}\right)\cup \left({A}\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
12 4 11 eqsstri ${⊢}{A}\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
13 coundi ${⊢}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)=\left(\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ {A}\right)\cup \left(\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)$
14 cossxp ${⊢}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ {A}\subseteq \mathrm{dom}{A}×\mathrm{ran}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)$
15 rnxpss ${⊢}\mathrm{ran}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{ran}{A}$
16 xpss2 ${⊢}\mathrm{ran}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{ran}{A}\to \mathrm{dom}{A}×\mathrm{ran}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
17 15 16 ax-mp ${⊢}\mathrm{dom}{A}×\mathrm{ran}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
18 14 17 sstri ${⊢}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ {A}\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
19 xptrrel ${⊢}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
20 18 19 unssi ${⊢}\left(\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ {A}\right)\cup \left(\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
21 13 20 eqsstri ${⊢}\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
22 12 21 unssi ${⊢}\left({A}\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\right)\cup \left(\left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
23 3 22 eqsstri ${⊢}\left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq \mathrm{dom}{A}×\mathrm{ran}{A}$
24 ssun2 ${⊢}\mathrm{dom}{A}×\mathrm{ran}{A}\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)$
25 23 24 sstri ${⊢}\left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)$
26 1 elexi ${⊢}{A}\in \mathrm{V}$
27 26 dmex ${⊢}\mathrm{dom}{A}\in \mathrm{V}$
28 26 rnex ${⊢}\mathrm{ran}{A}\in \mathrm{V}$
29 27 28 xpex ${⊢}\mathrm{dom}{A}×\mathrm{ran}{A}\in \mathrm{V}$
30 26 29 unex ${⊢}{A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\in \mathrm{V}$
31 trcleq2lem ${⊢}{x}={A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\to \left(\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)↔\left({A}\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\wedge \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\right)$
32 30 31 spcev ${⊢}\left({A}\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\wedge \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)$
33 intexab ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)↔\bigcap \left\{{x}|\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\in \mathrm{V}$
34 32 33 sylib ${⊢}\left({A}\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\wedge \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\circ \left({A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\subseteq {A}\cup \left(\mathrm{dom}{A}×\mathrm{ran}{A}\right)\right)\to \bigcap \left\{{x}|\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\in \mathrm{V}$
35 2 25 34 mp2an ${⊢}\bigcap \left\{{x}|\left({A}\subseteq {x}\wedge {x}\circ {x}\subseteq {x}\right)\right\}\in \mathrm{V}$