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 e. _V |-> U_ n e. N ( r ^r n ) )
Assertion iunrelexpuztr 
|- ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) -> ( ( C ` R ) o. ( C ` R ) ) C_ ( C ` R ) )

Proof

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