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{\uparrow }_{r}i\right)\right)$$
2		dfrcl4	$$⊢\mathrm{r*}=\left(b\in \mathrm{V}⟼\bigcup _{j\in \left\{0,1\right\}}\left(b{\uparrow }_{r}j\right)\right)$$
3		dfrcl4	$$⊢\mathrm{r*}=\left(c\in \mathrm{V}⟼\bigcup _{k\in \left\{0,1\right\}}\left(c{\uparrow }_{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{\uparrow }_{r}k=d{\uparrow }_{r}j$$
8	7	cbviunv	$$⊢\bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)$$
9		1ex	$$⊢1\in \mathrm{V}$$
10		oveq2	$$⊢i=1\to \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}1$$
11	9 10	iunxsn	$$⊢\bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}1$$
12		ovex	$$⊢d{\uparrow }_{r}j\in \mathrm{V}$$
13	4 12	iunex	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)\in \mathrm{V}$$
14		relexp1g	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)\in \mathrm{V}\to \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}1=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)$$
15	13 14	ax-mp	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}1=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)$$
16	11 15	eqtri	$$⊢\bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)$$
17	16	eqcomi	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)=\bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)$$
18	8 17	eqtri	$$⊢\bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)=\bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{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{\uparrow }_{r}j\right){\uparrow }_{r}i\right)\subseteq \bigcup _{i\in \left\{0,1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)$$
21	19 20	ax-mp	$$⊢\bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)\subseteq \bigcup _{i\in \left\{0,1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)$$
22	18 21	eqsstri	$$⊢\bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)\subseteq \bigcup _{i\in \left\{0,1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)$$
23		c0ex	$$⊢0\in \mathrm{V}$$
24	23	prid1	$$⊢0\in \left\{0,1\right\}$$
25		oveq2	$$⊢k=0\to d{\uparrow }_{r}k=d{\uparrow }_{r}0$$
26	25	ssiun2s	$$⊢0\in \left\{0,1\right\}\to d{\uparrow }_{r}0\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)$$
27	24 26	ax-mp	$$⊢d{\uparrow }_{r}0\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)$$
28		oveq2	$$⊢j=k\to d{\uparrow }_{r}j=d{\uparrow }_{r}k$$
29	28	cbviunv	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)=\bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)$$
30	29	eqimssi	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)$$
31		unss12	$$⊢\left(d{\uparrow }_{r}0\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)\wedge \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)\right)\to \left(d{\uparrow }_{r}0\right)\cup \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)\cup \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)$$
32	27 30 31	mp2an	$$⊢\left(d{\uparrow }_{r}0\right)\cup \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)\subseteq \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)\cup \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{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{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\bigcup _{i\in \left\{0\right\}\cup \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{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{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\bigcup _{i\in \left\{0\right\}\cup \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{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{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\bigcup _{i\in \left\{0\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)\cup \bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)$$
37		oveq2	$$⊢i=0\to \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}0$$
38	23 37	iunxsn	$$⊢\bigcup _{i\in \left\{0\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}0$$
39		vex	$$⊢d\in \mathrm{V}$$
40		0nn0	$$⊢0\in {\mathbb{N}}_0$$
41		1nn0	$$⊢1\in {\mathbb{N}}_0$$
42		prssi	$$⊢\left(0\in {\mathbb{N}}_0\wedge 1\in {\mathbb{N}}_0\right)\to \left\{0,1\right\}\subseteq {\mathbb{N}}_0$$
43	40 41 42	mp2an	$$⊢\left\{0,1\right\}\subseteq {\mathbb{N}}_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 {\mathbb{N}}_0\wedge \left\{0,1\right\}\cap \left\{0,1\right\}\ne \varnothing \right)\to \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}0=d{\uparrow }_{r}0$$
47	39 43 45 46	mp3an	$$⊢\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}0=d{\uparrow }_{r}0$$
48	38 47	eqtri	$$⊢\bigcup _{i\in \left\{0\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=d{\uparrow }_{r}0$$
49	48 16	uneq12i	$$⊢\bigcup _{i\in \left\{0\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)\cup \bigcup _{i\in \left\{1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\left(d{\uparrow }_{r}0\right)\cup \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{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{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\left(d{\uparrow }_{r}0\right)\cup \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)$$
51	35 50	eqtri	$$⊢\bigcup _{i\in \left\{0,1\right\}}\left(\bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right){\uparrow }_{r}i\right)=\left(d{\uparrow }_{r}0\right)\cup \bigcup _{j\in \left\{0,1\right\}}\left(d{\uparrow }_{r}j\right)$$
52		iunxun	$$⊢\bigcup _{k\in \left\{0,1\right\}\cup \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)=\bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)\cup \bigcup _{k\in \left\{0,1\right\}}\left(d{\uparrow }_{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{\uparrow }_{r}j\right){\uparrow }_{r}i\right)\subseteq \bigcup _{k\in \left\{0,1\right\}\cup \left\{0,1\right\}}\left(d{\uparrow }_{r}k\right)$$
54	1 2 3 4 4 6 22 22 53	comptiunov2i	$$⊢\mathrm{r*}\circ \mathrm{r*}=\mathrm{r*}$$