Theorem dfrcl4

Description: Reflexive closure of a relation as indexed union of powers of the relation. (Contributed by RP, 8-Jun-2020)

	Ref	Expression
Assertion	dfrcl4	$$⊢\mathrm{r*}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfrcl3	$$⊢\mathrm{r*}=\left(r\in \mathrm{V}⟼\left(r{\uparrow }_{r}0\right)\cup \left(r{\uparrow }_{r}1\right)\right)$$
2		df-pr	$$⊢\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}$$
3		iuneq1	$$⊢\left\{0,1\right\}=\left\{0\right\}\cup \left\{1\right\}\to \bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)=\bigcup _{n\in \left\{0\right\}\cup \left\{1\right\}}\left(r{\uparrow }_{r}n\right)$$
4	2 3	ax-mp	$$⊢\bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)=\bigcup _{n\in \left\{0\right\}\cup \left\{1\right\}}\left(r{\uparrow }_{r}n\right)$$
5		iunxun	$$⊢\bigcup _{n\in \left\{0\right\}\cup \left\{1\right\}}\left(r{\uparrow }_{r}n\right)=\bigcup _{n\in \left\{0\right\}}\left(r{\uparrow }_{r}n\right)\cup \bigcup _{n\in \left\{1\right\}}\left(r{\uparrow }_{r}n\right)$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7		oveq2	$$⊢n=0\to r{\uparrow }_{r}n=r{\uparrow }_{r}0$$
8	6 7	iunxsn	$$⊢\bigcup _{n\in \left\{0\right\}}\left(r{\uparrow }_{r}n\right)=r{\uparrow }_{r}0$$
9		1ex	$$⊢1\in \mathrm{V}$$
10		oveq2	$$⊢n=1\to r{\uparrow }_{r}n=r{\uparrow }_{r}1$$
11	9 10	iunxsn	$$⊢\bigcup _{n\in \left\{1\right\}}\left(r{\uparrow }_{r}n\right)=r{\uparrow }_{r}1$$
12	8 11	uneq12i	$$⊢\bigcup _{n\in \left\{0\right\}}\left(r{\uparrow }_{r}n\right)\cup \bigcup _{n\in \left\{1\right\}}\left(r{\uparrow }_{r}n\right)=\left(r{\uparrow }_{r}0\right)\cup \left(r{\uparrow }_{r}1\right)$$
13	4 5 12	3eqtri	$$⊢\bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)=\left(r{\uparrow }_{r}0\right)\cup \left(r{\uparrow }_{r}1\right)$$
14	13	mpteq2i	$$⊢\left(r\in \mathrm{V}⟼\bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)\right)=\left(r\in \mathrm{V}⟼\left(r{\uparrow }_{r}0\right)\cup \left(r{\uparrow }_{r}1\right)\right)$$
15	1 14	eqtr4i	$$⊢\mathrm{r*}=\left(r\in \mathrm{V}⟼\bigcup _{n\in \left\{0,1\right\}}\left(r{\uparrow }_{r}n\right)\right)$$