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*=rVrr0t+r

Proof

Step Hyp Ref Expression
1 dfrtrcl3 t*=rVn0rrn
2 df-n0 0=0
3 2 equncomi 0=0
4 iuneq1 0=0n0rrn=n0rrn
5 3 4 ax-mp n0rrn=n0rrn
6 iunxun n0rrn=n0rrnnrrn
7 5 6 eqtri n0rrn=n0rrnnrrn
8 c0ex 0V
9 oveq2 n=0rrn=rr0
10 8 9 iunxsn n0rrn=rr0
11 10 a1i rVn0rrn=rr0
12 oveq1 x=rxrn=rrn
13 12 iuneq2d x=rnxrn=nrrn
14 dftrcl3 t+=xVnxrn
15 nnex V
16 ovex rrnV
17 15 16 iunex nrrnV
18 13 14 17 fvmpt rVt+r=nrrn
19 18 eqcomd rVnrrn=t+r
20 11 19 uneq12d rVn0rrnnrrn=rr0t+r
21 7 20 eqtrid rVn0rrn=rr0t+r
22 21 mpteq2ia rVn0rrn=rVrr0t+r
23 1 22 eqtri t*=rVrr0t+r