# Metamath Proof Explorer

## Theorem cotrclrcl

Description: The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020)

Ref Expression
Assertion cotrclrcl ${⊢}\mathrm{t+}\circ \mathrm{r*}=\mathrm{t*}$

### Proof

Step Hyp Ref Expression
1 dftrcl3 ${⊢}\mathrm{t+}=\left({a}\in \mathrm{V}⟼\bigcup _{{i}\in ℕ}\left({a}{↑}_{r}{i}\right)\right)$
2 dfrcl4 ${⊢}\mathrm{r*}=\left({b}\in \mathrm{V}⟼\bigcup _{{j}\in \left\{0,1\right\}}\left({b}{↑}_{r}{j}\right)\right)$
3 dfrtrcl3 ${⊢}\mathrm{t*}=\left({c}\in \mathrm{V}⟼\bigcup _{{k}\in {ℕ}_{0}}\left({c}{↑}_{r}{k}\right)\right)$
4 nnex ${⊢}ℕ\in \mathrm{V}$
5 prex ${⊢}\left\{0,1\right\}\in \mathrm{V}$
6 df-n0 ${⊢}{ℕ}_{0}=ℕ\cup \left\{0\right\}$
7 df-pr ${⊢}\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}$
8 7 equncomi ${⊢}\left\{0,1\right\}=\left\{1\right\}\cup \left\{0\right\}$
9 8 uneq2i ${⊢}ℕ\cup \left\{0,1\right\}=ℕ\cup \left(\left\{1\right\}\cup \left\{0\right\}\right)$
10 unass ${⊢}\left(ℕ\cup \left\{1\right\}\right)\cup \left\{0\right\}=ℕ\cup \left(\left\{1\right\}\cup \left\{0\right\}\right)$
11 1nn ${⊢}1\in ℕ$
12 snssi ${⊢}1\in ℕ\to \left\{1\right\}\subseteq ℕ$
13 11 12 ax-mp ${⊢}\left\{1\right\}\subseteq ℕ$
14 ssequn2 ${⊢}\left\{1\right\}\subseteq ℕ↔ℕ\cup \left\{1\right\}=ℕ$
15 13 14 mpbi ${⊢}ℕ\cup \left\{1\right\}=ℕ$
16 15 uneq1i ${⊢}\left(ℕ\cup \left\{1\right\}\right)\cup \left\{0\right\}=ℕ\cup \left\{0\right\}$
17 9 10 16 3eqtr2ri ${⊢}ℕ\cup \left\{0\right\}=ℕ\cup \left\{0,1\right\}$
18 6 17 eqtri ${⊢}{ℕ}_{0}=ℕ\cup \left\{0,1\right\}$
19 oveq2 ${⊢}{k}={i}\to {d}{↑}_{r}{k}={d}{↑}_{r}{i}$
20 19 cbviunv ${⊢}\bigcup _{{k}\in ℕ}\left({d}{↑}_{r}{k}\right)=\bigcup _{{i}\in ℕ}\left({d}{↑}_{r}{i}\right)$
21 ss2iun ${⊢}\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}{d}{↑}_{r}{i}\subseteq \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\to \bigcup _{{i}\in ℕ}\left({d}{↑}_{r}{i}\right)\subseteq \bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
22 1ex ${⊢}1\in \mathrm{V}$
23 22 prid2 ${⊢}1\in \left\{0,1\right\}$
24 oveq2 ${⊢}{j}=1\to {d}{↑}_{r}{j}={d}{↑}_{r}1$
25 relexp1g ${⊢}{d}\in \mathrm{V}\to {d}{↑}_{r}1={d}$
26 25 elv ${⊢}{d}{↑}_{r}1={d}$
27 24 26 syl6eq ${⊢}{j}=1\to {d}{↑}_{r}{j}={d}$
28 27 ssiun2s ${⊢}1\in \left\{0,1\right\}\to {d}\subseteq \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
29 23 28 ax-mp ${⊢}{d}\subseteq \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
30 29 a1i ${⊢}{i}\in ℕ\to {d}\subseteq \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
31 ovex ${⊢}{d}{↑}_{r}{j}\in \mathrm{V}$
32 5 31 iunex ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\in \mathrm{V}$
33 32 a1i ${⊢}{i}\in ℕ\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\in \mathrm{V}$
34 nnnn0 ${⊢}{i}\in ℕ\to {i}\in {ℕ}_{0}$
35 30 33 34 relexpss1d ${⊢}{i}\in ℕ\to {d}{↑}_{r}{i}\subseteq \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}$
36 21 35 mprg ${⊢}\bigcup _{{i}\in ℕ}\left({d}{↑}_{r}{i}\right)\subseteq \bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
37 20 36 eqsstri ${⊢}\bigcup _{{k}\in ℕ}\left({d}{↑}_{r}{k}\right)\subseteq \bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
38 oveq2 ${⊢}{i}=1\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}1$
39 relexp1g ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\in \mathrm{V}\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}1=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
40 32 39 ax-mp ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}1=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
41 oveq2 ${⊢}{j}={k}\to {d}{↑}_{r}{j}={d}{↑}_{r}{k}$
42 41 cbviunv ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)=\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
43 40 42 eqtri ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}1=\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
44 38 43 syl6eq ${⊢}{i}=1\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}=\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
45 44 ssiun2s ${⊢}1\in ℕ\to \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\subseteq \bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
46 11 45 ax-mp ${⊢}\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\subseteq \bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
47 iunss ${⊢}\bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)↔\forall {i}\in ℕ\phantom{\rule{.4em}{0ex}}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
48 iuneq1 ${⊢}\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)=\bigcup _{{j}\in \left\{0\right\}\cup \left\{1\right\}}\left({d}{↑}_{r}{j}\right)$
49 7 48 ax-mp ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)=\bigcup _{{j}\in \left\{0\right\}\cup \left\{1\right\}}\left({d}{↑}_{r}{j}\right)$
50 iunxun ${⊢}\bigcup _{{j}\in \left\{0\right\}\cup \left\{1\right\}}\left({d}{↑}_{r}{j}\right)=\bigcup _{{j}\in \left\{0\right\}}\left({d}{↑}_{r}{j}\right)\cup \bigcup _{{j}\in \left\{1\right\}}\left({d}{↑}_{r}{j}\right)$
51 c0ex ${⊢}0\in \mathrm{V}$
52 oveq2 ${⊢}{j}=0\to {d}{↑}_{r}{j}={d}{↑}_{r}0$
53 51 52 iunxsn ${⊢}\bigcup _{{j}\in \left\{0\right\}}\left({d}{↑}_{r}{j}\right)={d}{↑}_{r}0$
54 22 24 iunxsn ${⊢}\bigcup _{{j}\in \left\{1\right\}}\left({d}{↑}_{r}{j}\right)={d}{↑}_{r}1$
55 53 54 uneq12i ${⊢}\bigcup _{{j}\in \left\{0\right\}}\left({d}{↑}_{r}{j}\right)\cup \bigcup _{{j}\in \left\{1\right\}}\left({d}{↑}_{r}{j}\right)=\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)$
56 49 50 55 3eqtri ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)=\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)$
57 56 oveq1i ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}=\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{i}$
58 oveq2 ${⊢}{x}=1\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}=\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}1$
59 58 sseq1d ${⊢}{x}=1\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)↔\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}1\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)$
60 oveq2 ${⊢}{x}={y}\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}=\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}$
61 60 sseq1d ${⊢}{x}={y}\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)↔\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)$
62 oveq2 ${⊢}{x}={y}+1\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}=\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}\left({y}+1\right)$
63 62 sseq1d ${⊢}{x}={y}+1\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)↔\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}\left({y}+1\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)$
64 oveq2 ${⊢}{x}={i}\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}=\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{i}$
65 64 sseq1d ${⊢}{x}={i}\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{x}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)↔\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{i}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)$
66 ovex ${⊢}{d}{↑}_{r}0\in \mathrm{V}$
67 ovex ${⊢}{d}{↑}_{r}1\in \mathrm{V}$
68 66 67 unex ${⊢}\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\in \mathrm{V}$
69 relexp1g ${⊢}\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\in \mathrm{V}\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}1=\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)$
70 68 69 ax-mp ${⊢}\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}1=\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)$
71 0nn0 ${⊢}0\in {ℕ}_{0}$
72 oveq2 ${⊢}{k}=0\to {d}{↑}_{r}{k}={d}{↑}_{r}0$
73 72 ssiun2s ${⊢}0\in {ℕ}_{0}\to {d}{↑}_{r}0\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
74 71 73 ax-mp ${⊢}{d}{↑}_{r}0\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
75 1nn0 ${⊢}1\in {ℕ}_{0}$
76 oveq2 ${⊢}{k}=1\to {d}{↑}_{r}{k}={d}{↑}_{r}1$
77 76 ssiun2s ${⊢}1\in {ℕ}_{0}\to {d}{↑}_{r}1\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
78 75 77 ax-mp ${⊢}{d}{↑}_{r}1\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
79 74 78 unssi ${⊢}\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
80 70 79 eqsstri ${⊢}\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}1\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
81 simpl ${⊢}\left({y}\in ℕ\wedge \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)\to {y}\in ℕ$
82 relexpsucnnr ${⊢}\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\in \mathrm{V}\wedge {y}\in ℕ\right)\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}\left({y}+1\right)=\left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)$
83 68 81 82 sylancr ${⊢}\left({y}\in ℕ\wedge \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}\left({y}+1\right)=\left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)$
84 coss1 ${⊢}\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)$
85 coundi ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)=\left(\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}0\right)\right)\cup \left(\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\right)$
86 relexp0g ${⊢}{d}\in \mathrm{V}\to {d}{↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}$
87 86 elv ${⊢}{d}{↑}_{r}0={\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}$
88 87 coeq2i ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}0\right)=\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)$
89 coiun1 ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)=\bigcup _{{k}\in {ℕ}_{0}}\left(\left({d}{↑}_{r}{k}\right)\circ \left({\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)\right)$
90 coires1 ${⊢}\left({d}{↑}_{r}{k}\right)\circ \left({\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)={\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}$
91 90 a1i ${⊢}{k}\in {ℕ}_{0}\to \left({d}{↑}_{r}{k}\right)\circ \left({\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)={\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}$
92 91 iuneq2i ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left(\left({d}{↑}_{r}{k}\right)\circ \left({\mathrm{I}↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)\right)=\bigcup _{{k}\in {ℕ}_{0}}\left({\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)$
93 88 89 92 3eqtri ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}0\right)=\bigcup _{{k}\in {ℕ}_{0}}\left({\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)$
94 ss2iun ${⊢}\forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\subseteq {d}{↑}_{r}{k}\to \bigcup _{{k}\in {ℕ}_{0}}\left({\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
95 resss ${⊢}{\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\subseteq {d}{↑}_{r}{k}$
96 95 a1i ${⊢}{k}\in {ℕ}_{0}\to {\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\subseteq {d}{↑}_{r}{k}$
97 94 96 mprg ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({\left({d}{↑}_{r}{k}\right)↾}_{\left(\mathrm{dom}{d}\cup \mathrm{ran}{d}\right)}\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
98 93 97 eqsstri ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}0\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
99 coiun1 ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)=\bigcup _{{k}\in {ℕ}_{0}}\left(\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\right)$
100 iunss2 ${⊢}\forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {i}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}{i}\to \bigcup _{{k}\in {ℕ}_{0}}\left(\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{i}\in {ℕ}_{0}}\left({d}{↑}_{r}{i}\right)$
101 peano2nn0 ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in {ℕ}_{0}$
102 sbcel1v
103 101 102 sylibr
104 vex ${⊢}{d}\in \mathrm{V}$
105 relexpaddss ${⊢}\left({k}\in {ℕ}_{0}\wedge 1\in {ℕ}_{0}\wedge {d}\in \mathrm{V}\right)\to \left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}\left({k}+1\right)$
106 75 104 105 mp3an23 ${⊢}{k}\in {ℕ}_{0}\to \left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}\left({k}+1\right)$
107 ovex ${⊢}{k}+1\in \mathrm{V}$
108 csbconstg
109 107 108 ax-mp
110 csbov2g
111 csbvarg
112 111 oveq2d
113 110 112 eqtrd
114 107 113 ax-mp
115 106 109 114 3sstr4g
116 sbcssg
117 107 116 ax-mp
118 115 117 sylibr
119 sbcan
120 103 118 119 sylanbrc
121 120 spesbcd ${⊢}{k}\in {ℕ}_{0}\to \exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {ℕ}_{0}\wedge \left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}{i}\right)$
122 df-rex ${⊢}\exists {i}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}{i}↔\exists {i}\phantom{\rule{.4em}{0ex}}\left({i}\in {ℕ}_{0}\wedge \left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}{i}\right)$
123 121 122 sylibr ${⊢}{k}\in {ℕ}_{0}\to \exists {i}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq {d}{↑}_{r}{i}$
124 100 123 mprg ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left(\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{i}\in {ℕ}_{0}}\left({d}{↑}_{r}{i}\right)$
125 99 124 eqsstri ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq \bigcup _{{i}\in {ℕ}_{0}}\left({d}{↑}_{r}{i}\right)$
126 oveq2 ${⊢}{i}={k}\to {d}{↑}_{r}{i}={d}{↑}_{r}{k}$
127 126 cbviunv ${⊢}\bigcup _{{i}\in {ℕ}_{0}}\left({d}{↑}_{r}{i}\right)=\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
128 125 127 sseqtri ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
129 98 128 unssi ${⊢}\left(\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}0\right)\right)\cup \left(\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
130 85 129 eqsstri ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
131 84 130 sstrdi ${⊢}\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
132 131 adantl ${⊢}\left({y}\in ℕ\wedge \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\right)\circ \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
133 83 132 eqsstrd ${⊢}\left({y}\in ℕ\wedge \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}\left({y}+1\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
134 133 ex ${⊢}{y}\in ℕ\to \left(\left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{y}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}\left({y}+1\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)\right)$
135 59 61 63 65 80 134 nnind ${⊢}{i}\in ℕ\to \left(\left({d}{↑}_{r}0\right)\cup \left({d}{↑}_{r}1\right)\right){↑}_{r}{i}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
136 57 135 eqsstrid ${⊢}{i}\in ℕ\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
137 47 136 mprgbir ${⊢}\bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\subseteq \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)$
138 iuneq1 ${⊢}{ℕ}_{0}=ℕ\cup \left\{0,1\right\}\to \bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)=\bigcup _{{k}\in ℕ\cup \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
139 18 138 ax-mp ${⊢}\bigcup _{{k}\in {ℕ}_{0}}\left({d}{↑}_{r}{k}\right)=\bigcup _{{k}\in ℕ\cup \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
140 137 139 sseqtri ${⊢}\bigcup _{{i}\in ℕ}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\subseteq \bigcup _{{k}\in ℕ\cup \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
141 1 2 3 4 5 18 37 46 140 comptiunov2i ${⊢}\mathrm{t+}\circ \mathrm{r*}=\mathrm{t*}$