Metamath Proof Explorer


Theorem cotrclrcl

Description: The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020)

Ref Expression
Assertion cotrclrcl t+ r* = t*

Proof

Step Hyp Ref Expression
1 dftrcl3 t+ = a V i a r i
2 dfrcl4 r* = b V j 0 1 b r j
3 dfrtrcl3 t* = c V k 0 c r k
4 nnex V
5 prex 0 1 V
6 df-n0 0 = 0
7 df-pr 0 1 = 0 1
8 7 equncomi 0 1 = 1 0
9 8 uneq2i 0 1 = 1 0
10 unass 1 0 = 1 0
11 1nn 1
12 snssi 1 1
13 11 12 ax-mp 1
14 ssequn2 1 1 =
15 13 14 mpbi 1 =
16 15 uneq1i 1 0 = 0
17 9 10 16 3eqtr2ri 0 = 0 1
18 6 17 eqtri 0 = 0 1
19 oveq2 k = i d r k = d r i
20 19 cbviunv k d r k = i d r i
21 ss2iun i d r i j 0 1 d r j r i i d r i i j 0 1 d r j r i
22 1ex 1 V
23 22 prid2 1 0 1
24 oveq2 j = 1 d r j = d r 1
25 relexp1g d V d r 1 = d
26 25 elv d r 1 = d
27 24 26 syl6eq j = 1 d r j = d
28 27 ssiun2s 1 0 1 d j 0 1 d r j
29 23 28 ax-mp d j 0 1 d r j
30 29 a1i i d j 0 1 d r j
31 ovex d r j V
32 5 31 iunex j 0 1 d r j V
33 32 a1i i j 0 1 d r j V
34 nnnn0 i i 0
35 30 33 34 relexpss1d i d r i j 0 1 d r j r i
36 21 35 mprg i d r i i j 0 1 d r j r i
37 20 36 eqsstri k d r k i j 0 1 d r j r i
38 oveq2 i = 1 j 0 1 d r j r i = j 0 1 d r j r 1
39 relexp1g j 0 1 d r j V j 0 1 d r j r 1 = j 0 1 d r j
40 32 39 ax-mp j 0 1 d r j r 1 = j 0 1 d r j
41 oveq2 j = k d r j = d r k
42 41 cbviunv j 0 1 d r j = k 0 1 d r k
43 40 42 eqtri j 0 1 d r j r 1 = k 0 1 d r k
44 38 43 syl6eq i = 1 j 0 1 d r j r i = k 0 1 d r k
45 44 ssiun2s 1 k 0 1 d r k i j 0 1 d r j r i
46 11 45 ax-mp k 0 1 d r k i j 0 1 d r j r i
47 iunss i j 0 1 d r j r i k 0 d r k i j 0 1 d r j r i k 0 d r k
48 iuneq1 0 1 = 0 1 j 0 1 d r j = j 0 1 d r j
49 7 48 ax-mp j 0 1 d r j = j 0 1 d r j
50 iunxun j 0 1 d r j = j 0 d r j j 1 d r j
51 c0ex 0 V
52 oveq2 j = 0 d r j = d r 0
53 51 52 iunxsn j 0 d r j = d r 0
54 22 24 iunxsn j 1 d r j = d r 1
55 53 54 uneq12i j 0 d r j j 1 d r j = d r 0 d r 1
56 49 50 55 3eqtri j 0 1 d r j = d r 0 d r 1
57 56 oveq1i j 0 1 d r j r i = d r 0 d r 1 r i
58 oveq2 x = 1 d r 0 d r 1 r x = d r 0 d r 1 r 1
59 58 sseq1d x = 1 d r 0 d r 1 r x k 0 d r k d r 0 d r 1 r 1 k 0 d r k
60 oveq2 x = y d r 0 d r 1 r x = d r 0 d r 1 r y
61 60 sseq1d x = y d r 0 d r 1 r x k 0 d r k d r 0 d r 1 r y k 0 d r k
62 oveq2 x = y + 1 d r 0 d r 1 r x = d r 0 d r 1 r y + 1
63 62 sseq1d x = y + 1 d r 0 d r 1 r x k 0 d r k d r 0 d r 1 r y + 1 k 0 d r k
64 oveq2 x = i d r 0 d r 1 r x = d r 0 d r 1 r i
65 64 sseq1d x = i d r 0 d r 1 r x k 0 d r k d r 0 d r 1 r i k 0 d r k
66 ovex d r 0 V
67 ovex d r 1 V
68 66 67 unex d r 0 d r 1 V
69 relexp1g d r 0 d r 1 V d r 0 d r 1 r 1 = d r 0 d r 1
70 68 69 ax-mp d r 0 d r 1 r 1 = d r 0 d r 1
71 0nn0 0 0
72 oveq2 k = 0 d r k = d r 0
73 72 ssiun2s 0 0 d r 0 k 0 d r k
74 71 73 ax-mp d r 0 k 0 d r k
75 1nn0 1 0
76 oveq2 k = 1 d r k = d r 1
77 76 ssiun2s 1 0 d r 1 k 0 d r k
78 75 77 ax-mp d r 1 k 0 d r k
79 74 78 unssi d r 0 d r 1 k 0 d r k
80 70 79 eqsstri d r 0 d r 1 r 1 k 0 d r k
81 simpl y d r 0 d r 1 r y k 0 d r k y
82 relexpsucnnr d r 0 d r 1 V y d r 0 d r 1 r y + 1 = d r 0 d r 1 r y d r 0 d r 1
83 68 81 82 sylancr y d r 0 d r 1 r y k 0 d r k d r 0 d r 1 r y + 1 = d r 0 d r 1 r y d r 0 d r 1
84 coss1 d r 0 d r 1 r y k 0 d r k d r 0 d r 1 r y d r 0 d r 1 k 0 d r k d r 0 d r 1
85 coundi k 0 d r k d r 0 d r 1 = k 0 d r k d r 0 k 0 d r k d r 1
86 relexp0g d V d r 0 = I dom d ran d
87 86 elv d r 0 = I dom d ran d
88 87 coeq2i k 0 d r k d r 0 = k 0 d r k I dom d ran d
89 coiun1 k 0 d r k I dom d ran d = k 0 d r k I dom d ran d
90 coires1 d r k I dom d ran d = d r k dom d ran d
91 90 a1i k 0 d r k I dom d ran d = d r k dom d ran d
92 91 iuneq2i k 0 d r k I dom d ran d = k 0 d r k dom d ran d
93 88 89 92 3eqtri k 0 d r k d r 0 = k 0 d r k dom d ran d
94 ss2iun k 0 d r k dom d ran d d r k k 0 d r k dom d ran d k 0 d r k
95 resss d r k dom d ran d d r k
96 95 a1i k 0 d r k dom d ran d d r k
97 94 96 mprg k 0 d r k dom d ran d k 0 d r k
98 93 97 eqsstri k 0 d r k d r 0 k 0 d r k
99 coiun1 k 0 d r k d r 1 = k 0 d r k d r 1
100 iunss2 k 0 i 0 d r k d r 1 d r i k 0 d r k d r 1 i 0 d r i
101 peano2nn0 k 0 k + 1 0
102 sbcel1v [˙k + 1 / i]˙ i 0 k + 1 0
103 101 102 sylibr k 0 [˙k + 1 / i]˙ i 0
104 vex d V
105 relexpaddss k 0 1 0 d V d r k d r 1 d r k + 1
106 75 104 105 mp3an23 k 0 d r k d r 1 d r k + 1
107 ovex k + 1 V
108 csbconstg k + 1 V k + 1 / i d r k d r 1 = d r k d r 1
109 107 108 ax-mp k + 1 / i d r k d r 1 = d r k d r 1
110 csbov2g k + 1 V k + 1 / i d r i = d r k + 1 / i i
111 csbvarg k + 1 V k + 1 / i i = k + 1
112 111 oveq2d k + 1 V d r k + 1 / i i = d r k + 1
113 110 112 eqtrd k + 1 V k + 1 / i d r i = d r k + 1
114 107 113 ax-mp k + 1 / i d r i = d r k + 1
115 106 109 114 3sstr4g k 0 k + 1 / i d r k d r 1 k + 1 / i d r i
116 sbcssg k + 1 V [˙k + 1 / i]˙ d r k d r 1 d r i k + 1 / i d r k d r 1 k + 1 / i d r i
117 107 116 ax-mp [˙k + 1 / i]˙ d r k d r 1 d r i k + 1 / i d r k d r 1 k + 1 / i d r i
118 115 117 sylibr k 0 [˙k + 1 / i]˙ d r k d r 1 d r i
119 sbcan [˙k + 1 / i]˙ i 0 d r k d r 1 d r i [˙k + 1 / i]˙ i 0 [˙k + 1 / i]˙ d r k d r 1 d r i
120 103 118 119 sylanbrc k 0 [˙k + 1 / i]˙ i 0 d r k d r 1 d r i
121 120 spesbcd k 0 i i 0 d r k d r 1 d r i
122 df-rex i 0 d r k d r 1 d r i i i 0 d r k d r 1 d r i
123 121 122 sylibr k 0 i 0 d r k d r 1 d r i
124 100 123 mprg k 0 d r k d r 1 i 0 d r i
125 99 124 eqsstri k 0 d r k d r 1 i 0 d r i
126 oveq2 i = k d r i = d r k
127 126 cbviunv i 0 d r i = k 0 d r k
128 125 127 sseqtri k 0 d r k d r 1 k 0 d r k
129 98 128 unssi k 0 d r k d r 0 k 0 d r k d r 1 k 0 d r k
130 85 129 eqsstri k 0 d r k d r 0 d r 1 k 0 d r k
131 84 130 sstrdi d r 0 d r 1 r y k 0 d r k d r 0 d r 1 r y d r 0 d r 1 k 0 d r k
132 131 adantl y d r 0 d r 1 r y k 0 d r k d r 0 d r 1 r y d r 0 d r 1 k 0 d r k
133 83 132 eqsstrd y d r 0 d r 1 r y k 0 d r k d r 0 d r 1 r y + 1 k 0 d r k
134 133 ex y d r 0 d r 1 r y k 0 d r k d r 0 d r 1 r y + 1 k 0 d r k
135 59 61 63 65 80 134 nnind i d r 0 d r 1 r i k 0 d r k
136 57 135 eqsstrid i j 0 1 d r j r i k 0 d r k
137 47 136 mprgbir i j 0 1 d r j r i k 0 d r k
138 iuneq1 0 = 0 1 k 0 d r k = k 0 1 d r k
139 18 138 ax-mp k 0 d r k = k 0 1 d r k
140 137 139 sseqtri i j 0 1 d r j r i k 0 1 d r k
141 1 2 3 4 5 18 37 46 140 comptiunov2i t+ r* = t*