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	|- r* = ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) )

Proof

Step	Hyp	Ref	Expression
1		dfrcl3	|- r* = ( r e. _V |-> ( ( r ^r 0 ) u. ( r ^r 1 ) ) )
2		df-pr	|- { 0 , 1 } = ( { 0 } u. { 1 } )
3		iuneq1	|- ( { 0 , 1 } = ( { 0 } u. { 1 } ) -> U_ n e. { 0 , 1 } ( r ^r n ) = U_ n e. ( { 0 } u. { 1 } ) ( r ^r n ) )
4	2 3	ax-mp	|- U_ n e. { 0 , 1 } ( r ^r n ) = U_ n e. ( { 0 } u. { 1 } ) ( r ^r n )
5		iunxun	|- U_ n e. ( { 0 } u. { 1 } ) ( r ^r n ) = ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. { 1 } ( r ^r n ) )
6		c0ex	|- 0 e. _V
7		oveq2	|- ( n = 0 -> ( r ^r n ) = ( r ^r 0 ) )
8	6 7	iunxsn	|- U_ n e. { 0 } ( r ^r n ) = ( r ^r 0 )
9		1ex	|- 1 e. _V
10		oveq2	|- ( n = 1 -> ( r ^r n ) = ( r ^r 1 ) )
11	9 10	iunxsn	|- U_ n e. { 1 } ( r ^r n ) = ( r ^r 1 )
12	8 11	uneq12i	|- ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. { 1 } ( r ^r n ) ) = ( ( r ^r 0 ) u. ( r ^r 1 ) )
13	4 5 12	3eqtri	|- U_ n e. { 0 , 1 } ( r ^r n ) = ( ( r ^r 0 ) u. ( r ^r 1 ) )
14	13	mpteq2i	|- ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) ) = ( r e. _V |-> ( ( r ^r 0 ) u. ( r ^r 1 ) ) )
15	1 14	eqtr4i	|- r* = ( r e. _V |-> U_ n e. { 0 , 1 } ( r ^r n ) )