Theorem dfrcl3

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

	Ref	Expression
Assertion	dfrcl3	|- r* = ( x e. _V |-> ( ( x ^r 0 ) u. ( x ^r 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfrcl2	|- r* = ( x e. _V |-> ( ( _I |` ( dom x u. ran x ) ) u. x ) )
2		relexp0g	|- ( x e. _V -> ( x ^r 0 ) = ( _I |` ( dom x u. ran x ) ) )
3		relexp1g	|- ( x e. _V -> ( x ^r 1 ) = x )
4	2 3	uneq12d	|- ( x e. _V -> ( ( x ^r 0 ) u. ( x ^r 1 ) ) = ( ( _I |` ( dom x u. ran x ) ) u. x ) )
5	4	mpteq2ia	|- ( x e. _V |-> ( ( x ^r 0 ) u. ( x ^r 1 ) ) ) = ( x e. _V |-> ( ( _I |` ( dom x u. ran x ) ) u. x ) )
6	1 5	eqtr4i	|- r* = ( x e. _V |-> ( ( x ^r 0 ) u. ( x ^r 1 ) ) )