Metamath Proof Explorer


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 syl5eq
 |-  ( 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 ) ) )