Theorem dfid6

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

	Ref	Expression
Assertion	dfid6	|- _I = ( x e. _V |-> U_ n e. { 1 } ( x ^r n ) )

Proof

Step	Hyp	Ref	Expression
1		dfid4	|- _I = ( x e. _V |-> x )
2		1ex	|- 1 e. _V
3		oveq2	|- ( n = 1 -> ( x ^r n ) = ( x ^r 1 ) )
4	2 3	iunxsn	|- U_ n e. { 1 } ( x ^r n ) = ( x ^r 1 )
5		relexp1g	|- ( x e. _V -> ( x ^r 1 ) = x )
6	4 5	eqtrid	|- ( x e. _V -> U_ n e. { 1 } ( x ^r n ) = x )
7	6	mpteq2ia	|- ( x e. _V |-> U_ n e. { 1 } ( x ^r n ) ) = ( x e. _V |-> x )
8	1 7	eqtr4i	|- _I = ( x e. _V |-> U_ n e. { 1 } ( x ^r n ) )