Theorem dfrtrcl4

Description: Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020)

	Ref	Expression
Assertion	dfrtrcl4	|- t* = ( r e. _V |-> ( ( r ^r 0 ) u. ( t+ ` r ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfrtrcl3	|- t* = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
2		df-n0	|- NN0 = ( NN u. { 0 } )
3	2	equncomi	|- NN0 = ( { 0 } u. NN )
4		iuneq1	|- ( NN0 = ( { 0 } u. NN ) -> U_ n e. NN0 ( r ^r n ) = U_ n e. ( { 0 } u. NN ) ( r ^r n ) )
5	3 4	ax-mp	|- U_ n e. NN0 ( r ^r n ) = U_ n e. ( { 0 } u. NN ) ( r ^r n )
6		iunxun	|- U_ n e. ( { 0 } u. NN ) ( r ^r n ) = ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. NN ( r ^r n ) )
7	5 6	eqtri	|- U_ n e. NN0 ( r ^r n ) = ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. NN ( r ^r n ) )
8		c0ex	|- 0 e. _V
9		oveq2	|- ( n = 0 -> ( r ^r n ) = ( r ^r 0 ) )
10	8 9	iunxsn	|- U_ n e. { 0 } ( r ^r n ) = ( r ^r 0 )
11	10	a1i	|- ( r e. _V -> U_ n e. { 0 } ( r ^r n ) = ( r ^r 0 ) )
12		oveq1	|- ( x = r -> ( x ^r n ) = ( r ^r n ) )
13	12	iuneq2d	|- ( x = r -> U_ n e. NN ( x ^r n ) = U_ n e. NN ( r ^r n ) )
14		dftrcl3	|- t+ = ( x e. _V |-> U_ n e. NN ( x ^r n ) )
15		nnex	|- NN e. _V
16		ovex	|- ( r ^r n ) e. _V
17	15 16	iunex	|- U_ n e. NN ( r ^r n ) e. _V
18	13 14 17	fvmpt	|- ( r e. _V -> ( t+ ` r ) = U_ n e. NN ( r ^r n ) )
19	18	eqcomd	|- ( r e. _V -> U_ n e. NN ( r ^r n ) = ( t+ ` r ) )
20	11 19	uneq12d	|- ( r e. _V -> ( U_ n e. { 0 } ( r ^r n ) u. U_ n e. NN ( r ^r n ) ) = ( ( r ^r 0 ) u. ( t+ ` r ) ) )
21	7 20	eqtrid	|- ( r e. _V -> U_ n e. NN0 ( r ^r n ) = ( ( r ^r 0 ) u. ( t+ ` r ) ) )
22	21	mpteq2ia	|- ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) = ( r e. _V |-> ( ( r ^r 0 ) u. ( t+ ` r ) ) )
23	1 22	eqtri	|- t* = ( r e. _V |-> ( ( r ^r 0 ) u. ( t+ ` r ) ) )