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 
 |-  z e. _V
17 vex 
 |-  y e. _V
18 brcogw 
 |-  ( ( ( x e. _V /\ z e. _V /\ y e. _V ) /\ ( x ( R ^r i ) y /\ y ( R ^r j ) z ) ) -> x ( ( R ^r j ) o. ( R ^r i ) ) z )
19 18 ex 
 |-  ( ( x e. _V /\ z e. _V /\ y e. _V ) -> ( ( x ( R ^r i ) y /\ y ( R ^r j ) z ) -> x ( ( R ^r j ) o. ( R ^r i ) ) z ) )
20 15 16 17 19 mp3an 
 |-  ( ( x ( R ^r i ) y /\ y ( R ^r j ) z ) -> x ( ( R ^r j ) o. ( R ^r i ) ) z )
21 simpll3 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> M e. NN0 )
22 simprr 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
23 simpll2 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> N = ( ZZ>= ` M ) )
24 22 23 eleqtrd 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> j e. ( ZZ>= ` M ) )
25 eluznn0 
 |-  ( ( M e. NN0 /\ j e. ( ZZ>= ` M ) ) -> j e. NN0 )
26 21 24 25 syl2anc 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> j e. NN0 )
27 simprl 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
28 27 23 eleqtrd 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> i e. ( ZZ>= ` M ) )
29 21 28 9 syl2anc 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> i e. NN0 )
30 simpll1 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> R e. V )
31 relexpaddss 
 |-  ( ( j e. NN0 /\ i e. NN0 /\ R e. V ) -> ( ( R ^r j ) o. ( R ^r i ) ) C_ ( R ^r ( j + i ) ) )
32 26 29 30 31 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 ) ) )
33 simplr 
 |-  ( ( ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) /\ n = ( j + i ) ) /\ ( i e. N /\ j e. N ) ) -> n = ( j + i ) )
34 33 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 ) ) )
35 32 34 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 ) )
36 35 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 ) )
37 20 36 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 ) )
38 37 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 )
39 14 38 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 ) )
40 39 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 ) ) )
41 2 40 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 ) ) )
42 41 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 ) ) )
43 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 ) )
44 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 ) ) )
45 43 44 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 ) ) )
46 df-rex 
 |-  ( E. n e. N x ( R ^r n ) z <-> E. n ( n e. N /\ x ( R ^r n ) z ) )
47 42 45 46 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 ) )
48 47 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 ) )
49 48 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 ) )
50 49 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 ) )
51 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 ) )
52 1 briunov2uz 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) ) -> ( x ( C ` R ) y <-> E. n e. 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 
 |-  ( E. n e. N x ( R ^r n ) y <-> E. i e. N x ( R ^r i ) y )
56 52 55 bitrdi 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) ) -> ( x ( C ` R ) y <-> E. i e. N x ( R ^r i ) y ) )
57 1 briunov2uz 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) ) -> ( y ( C ` R ) z <-> E. n e. 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 
 |-  ( E. n e. N y ( R ^r n ) z <-> E. j e. N y ( R ^r j ) z )
61 57 60 bitrdi 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) ) -> ( y ( C ` R ) z <-> E. j e. N y ( R ^r j ) z ) )
62 56 61 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 ) ) )
63 1 briunov2uz 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) ) -> ( x ( C ` R ) z <-> E. n e. N x ( R ^r n ) z ) )
64 62 63 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 ) ) )
65 64 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 ) ) )
66 65 albidv 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) ) -> ( A. y A. z ( ( x ( C ` R ) y /\ y ( C ` R ) z ) -> x ( C ` R ) z ) <-> 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 ) ) )
67 66 albidv 
 |-  ( ( 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 ) ) )
68 51 67 syl5bb 
 |-  ( ( 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 ) ) )
69 68 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 ) ) )
70 69 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 ) ) )
71 50 70 mpd 
 |-  ( ( R e. V /\ N = ( ZZ>= ` M ) /\ M e. NN0 ) -> ( ( C ` R ) o. ( C ` R ) ) C_ ( C ` R ) )