Metamath Proof Explorer


Theorem iunrelexpuztr

Description: The indexed union of relation exponentiation over upper integers is a transive relation. Generalized from rtrclreclem3 . (Contributed by RP, 4-Jun-2020)

Ref Expression
Hypothesis mptiunrelexp.def C = r V n N r r n
Assertion iunrelexpuztr R V N = M M 0 C R C R C R

Proof

Step Hyp Ref Expression
1 mptiunrelexp.def C = r V n N r r n
2 ovexd R V N = M M 0 j + i V
3 simprlr R V N = M M 0 n = j + i i N j N x R r i y y R r j z j N
4 simpll2 R V N = M M 0 n = j + i i N j N x R r i y y R r j z N = M
5 3 4 eleqtrd R V N = M M 0 n = j + i i N j N x R r i y y R r j z j M
6 simpll3 R V N = M M 0 n = j + i i N j N x R r i y y R r j z M 0
7 simprll R V N = M M 0 n = j + i i N j N x R r i y y R r j z i N
8 7 4 eleqtrd R V N = M M 0 n = j + i i N j N x R r i y y R r j z i M
9 eluznn0 M 0 i M i 0
10 6 8 9 syl2anc R V N = M M 0 n = j + i i N j N x R r i y y R r j z i 0
11 uzaddcl j M i 0 j + i M
12 5 10 11 syl2anc R V N = M M 0 n = j + i i N j N x R r i y y R r j z j + i M
13 simplr R V N = M M 0 n = j + i i N j N x R r i y y R r j z n = j + i
14 12 13 4 3eltr4d R V N = M M 0 n = j + i i N j N x R r i y y R r j z n N
15 vex x V
16 vex z V
17 vex y V
18 brcogw x V z V y V x R r i y y R r j z x R r j R r i z
19 18 ex x V z V y V x R r i y y R r j z x R r j R r i z
20 15 16 17 19 mp3an x R r i y y R r j z x R r j R r i z
21 simpll3 R V N = M M 0 n = j + i i N j N M 0
22 simprr R V N = M M 0 n = j + i i N j N j N
23 simpll2 R V N = M M 0 n = j + i i N j N N = M
24 22 23 eleqtrd R V N = M M 0 n = j + i i N j N j M
25 eluznn0 M 0 j M j 0
26 21 24 25 syl2anc R V N = M M 0 n = j + i i N j N j 0
27 simprl R V N = M M 0 n = j + i i N j N i N
28 27 23 eleqtrd R V N = M M 0 n = j + i i N j N i M
29 21 28 9 syl2anc R V N = M M 0 n = j + i i N j N i 0
30 simpll1 R V N = M M 0 n = j + i i N j N R V
31 relexpaddss j 0 i 0 R V R r j R r i R r j + i
32 26 29 30 31 syl3anc R V N = M M 0 n = j + i i N j N R r j R r i R r j + i
33 simplr R V N = M M 0 n = j + i i N j N n = j + i
34 33 oveq2d R V N = M M 0 n = j + i i N j N R r n = R r j + i
35 32 34 sseqtrrd R V N = M M 0 n = j + i i N j N R r j R r i R r n
36 35 ssbrd R V N = M M 0 n = j + i i N j N x R r j R r i z x R r n z
37 20 36 syl5 R V N = M M 0 n = j + i i N j N x R r i y y R r j z x R r n z
38 37 impr R V N = M M 0 n = j + i i N j N x R r i y y R r j z x R r n z
39 14 38 jca R V N = M M 0 n = j + i i N j N x R r i y y R r j z n N x R r n z
40 39 ex R V N = M M 0 n = j + i i N j N x R r i y y R r j z n N x R r n z
41 2 40 spcimedv R V N = M M 0 i N j N x R r i y y R r j z n n N x R r n z
42 41 exlimdvv R V N = M M 0 i j i N j N x R r i y y R r j z n n N x R r n z
43 reeanv i N j N x R r i y y R r j z i N x R r i y j N y R r j z
44 r2ex i N j N x R r i y y R r j z i j i N j N x R r i y y R r j z
45 43 44 bitr3i i N x R r i y j N y R r j z i j i N j N x R r i y y R r j z
46 df-rex n N x R r n z n n N x R r n z
47 42 45 46 3imtr4g R V N = M M 0 i N x R r i y j N y R r j z n N x R r n z
48 47 alrimiv R V N = M M 0 z i N x R r i y j N y R r j z n N x R r n z
49 48 alrimiv R V N = M M 0 y z i N x R r i y j N y R r j z n N x R r n z
50 49 alrimiv R V N = M M 0 x y z i N x R r i y j N y R r j z n N x R r n z
51 cotr C R C R C R x y z x C R y y C R z x C R z
52 1 briunov2uz R V N = M x C R y n N x R r n y
53 oveq2 n = i R r n = R r i
54 53 breqd n = i x R r n y x R r i y
55 54 cbvrexvw n N x R r n y i N x R r i y
56 52 55 bitrdi R V N = M x C R y i N x R r i y
57 1 briunov2uz R V N = M y C R z n N y R r n z
58 oveq2 n = j R r n = R r j
59 58 breqd n = j y R r n z y R r j z
60 59 cbvrexvw n N y R r n z j N y R r j z
61 57 60 bitrdi R V N = M y C R z j N y R r j z
62 56 61 anbi12d R V N = M x C R y y C R z i N x R r i y j N y R r j z
63 1 briunov2uz R V N = M x C R z n N x R r n z
64 62 63 imbi12d R V N = M x C R y y C R z x C R z i N x R r i y j N y R r j z n N x R r n z
65 64 albidv R V N = M z x C R y y C R z x C R z z i N x R r i y j N y R r j z n N x R r n z
66 65 albidv R V N = M y z x C R y y C R z x C R z y z i N x R r i y j N y R r j z n N x R r n z
67 66 albidv R V N = M x y z x C R y y C R z x C R z x y z i N x R r i y j N y R r j z n N x R r n z
68 51 67 syl5bb R V N = M C R C R C R x y z i N x R r i y j N y R r j z n N x R r n z
69 68 biimprd R V N = M x y z i N x R r i y j N y R r j z n N x R r n z C R C R C R
70 69 3adant3 R V N = M M 0 x y z i N x R r i y j N y R r j z n N x R r n z C R C R C R
71 50 70 mpd R V N = M M 0 C R C R C R