# Metamath Proof Explorer

## Theorem corclrcl

Description: The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion corclrcl ${⊢}\mathrm{r*}\circ \mathrm{r*}=\mathrm{r*}$

### Proof

Step Hyp Ref Expression
1 dfrcl4 ${⊢}\mathrm{r*}=\left({a}\in \mathrm{V}⟼\bigcup _{{i}\in \left\{0,1\right\}}\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 dfrcl4 ${⊢}\mathrm{r*}=\left({c}\in \mathrm{V}⟼\bigcup _{{k}\in \left\{0,1\right\}}\left({c}{↑}_{r}{k}\right)\right)$
4 prex ${⊢}\left\{0,1\right\}\in \mathrm{V}$
5 unidm ${⊢}\left\{0,1\right\}\cup \left\{0,1\right\}=\left\{0,1\right\}$
6 5 eqcomi ${⊢}\left\{0,1\right\}=\left\{0,1\right\}\cup \left\{0,1\right\}$
7 oveq2 ${⊢}{k}={j}\to {d}{↑}_{r}{k}={d}{↑}_{r}{j}$
8 7 cbviunv ${⊢}\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
9 1ex ${⊢}1\in \mathrm{V}$
10 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$
11 9 10 iunxsn ${⊢}\bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}1$
12 ovex ${⊢}{d}{↑}_{r}{j}\in \mathrm{V}$
13 4 12 iunex ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\in \mathrm{V}$
14 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)$
15 13 14 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)$
16 11 15 eqtri ${⊢}\bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
17 16 eqcomi ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)=\bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
18 8 17 eqtri ${⊢}\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)=\bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
19 snsspr2 ${⊢}\left\{1\right\}\subseteq \left\{0,1\right\}$
20 iunss1 ${⊢}\left\{1\right\}\subseteq \left\{0,1\right\}\to \bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\subseteq \bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
21 19 20 ax-mp ${⊢}\bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\subseteq \bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
22 18 21 eqsstri ${⊢}\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\subseteq \bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
23 c0ex ${⊢}0\in \mathrm{V}$
24 23 prid1 ${⊢}0\in \left\{0,1\right\}$
25 oveq2 ${⊢}{k}=0\to {d}{↑}_{r}{k}={d}{↑}_{r}0$
26 25 ssiun2s ${⊢}0\in \left\{0,1\right\}\to {d}{↑}_{r}0\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
27 24 26 ax-mp ${⊢}{d}{↑}_{r}0\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
28 oveq2 ${⊢}{j}={k}\to {d}{↑}_{r}{j}={d}{↑}_{r}{k}$
29 28 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)$
30 29 eqimssi ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
31 unss12 ${⊢}\left({d}{↑}_{r}0\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\wedge \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\right)\to \left({d}{↑}_{r}0\right)\cup \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\cup \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
32 27 30 31 mp2an ${⊢}\left({d}{↑}_{r}0\right)\cup \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)\subseteq \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\cup \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
33 df-pr ${⊢}\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}$
34 iuneq1 ${⊢}\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}\to \bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\bigcup _{{i}\in \left\{0\right\}\cup \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
35 33 34 ax-mp ${⊢}\bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\bigcup _{{i}\in \left\{0\right\}\cup \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
36 iunxun ${⊢}\bigcup _{{i}\in \left\{0\right\}\cup \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\bigcup _{{i}\in \left\{0\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\cup \bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)$
37 oveq2 ${⊢}{i}=0\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}0$
38 23 37 iunxsn ${⊢}\bigcup _{{i}\in \left\{0\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}0$
39 vex ${⊢}{d}\in \mathrm{V}$
40 0nn0 ${⊢}0\in {ℕ}_{0}$
41 1nn0 ${⊢}1\in {ℕ}_{0}$
42 prssi ${⊢}\left(0\in {ℕ}_{0}\wedge 1\in {ℕ}_{0}\right)\to \left\{0,1\right\}\subseteq {ℕ}_{0}$
43 40 41 42 mp2an ${⊢}\left\{0,1\right\}\subseteq {ℕ}_{0}$
44 24 24 elini ${⊢}0\in \left(\left\{0,1\right\}\cap \left\{0,1\right\}\right)$
45 44 ne0ii ${⊢}\left\{0,1\right\}\cap \left\{0,1\right\}\ne \varnothing$
46 iunrelexp0 ${⊢}\left({d}\in \mathrm{V}\wedge \left\{0,1\right\}\subseteq {ℕ}_{0}\wedge \left\{0,1\right\}\cap \left\{0,1\right\}\ne \varnothing \right)\to \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}0={d}{↑}_{r}0$
47 39 43 45 46 mp3an ${⊢}\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}0={d}{↑}_{r}0$
48 38 47 eqtri ${⊢}\bigcup _{{i}\in \left\{0\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)={d}{↑}_{r}0$
49 48 16 uneq12i ${⊢}\bigcup _{{i}\in \left\{0\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\cup \bigcup _{{i}\in \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\left({d}{↑}_{r}0\right)\cup \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
50 36 49 eqtri ${⊢}\bigcup _{{i}\in \left\{0\right\}\cup \left\{1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\left({d}{↑}_{r}0\right)\cup \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
51 35 50 eqtri ${⊢}\bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)=\left({d}{↑}_{r}0\right)\cup \bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right)$
52 iunxun ${⊢}\bigcup _{{k}\in \left\{0,1\right\}\cup \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)=\bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)\cup \bigcup _{{k}\in \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
53 32 51 52 3sstr4i ${⊢}\bigcup _{{i}\in \left\{0,1\right\}}\left(\bigcup _{{j}\in \left\{0,1\right\}}\left({d}{↑}_{r}{j}\right){↑}_{r}{i}\right)\subseteq \bigcup _{{k}\in \left\{0,1\right\}\cup \left\{0,1\right\}}\left({d}{↑}_{r}{k}\right)$
54 1 2 3 4 4 6 22 22 53 comptiunov2i ${⊢}\mathrm{r*}\circ \mathrm{r*}=\mathrm{r*}$