Theorem dfid6

Description: Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020)

	Ref	Expression
Assertion	dfid6	$$⊢\mathrm{I}=\left(x\in \mathrm{V}⟼\bigcup _{n\in \left\{1\right\}}\left(x{\uparrow }_{r}n\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfid4	$$⊢\mathrm{I}=\left(x\in \mathrm{V}⟼x\right)$$
2		1ex	$$⊢1\in \mathrm{V}$$
3		oveq2	$$⊢n=1\to x{\uparrow }_{r}n=x{\uparrow }_{r}1$$
4	2 3	iunxsn	$$⊢\bigcup _{n\in \left\{1\right\}}\left(x{\uparrow }_{r}n\right)=x{\uparrow }_{r}1$$
5		relexp1g	$$⊢x\in \mathrm{V}\to x{\uparrow }_{r}1=x$$
6	4 5	syl5eq	$$⊢x\in \mathrm{V}\to \bigcup _{n\in \left\{1\right\}}\left(x{\uparrow }_{r}n\right)=x$$
7	6	mpteq2ia	$$⊢\left(x\in \mathrm{V}⟼\bigcup _{n\in \left\{1\right\}}\left(x{\uparrow }_{r}n\right)\right)=\left(x\in \mathrm{V}⟼x\right)$$
8	1 7	eqtr4i	$$⊢\mathrm{I}=\left(x\in \mathrm{V}⟼\bigcup _{n\in \left\{1\right\}}\left(x{\uparrow }_{r}n\right)\right)$$