Metamath Proof Explorer

Theorem trclrelexplem

Description: The union of relational powers to positive multiples of N is a subset to the transitive closure raised to the power of N . (Contributed by RP, 15-Jun-2020)

Ref Expression
Assertion trclrelexplem 
|- ( N e. NN -> U_ k e. NN ( ( D ^r k ) ^r N ) C_ ( U_ j e. NN ( D ^r j ) ^r N ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 1 -> ( ( D ^r k ) ^r x ) = ( ( D ^r k ) ^r 1 ) )
2 1 iuneq2d 
 |-  ( x = 1 -> U_ k e. NN ( ( D ^r k ) ^r x ) = U_ k e. NN ( ( D ^r k ) ^r 1 ) )
3 oveq2 
 |-  ( x = 1 -> ( U_ j e. NN ( D ^r j ) ^r x ) = ( U_ j e. NN ( D ^r j ) ^r 1 ) )
4 2 3 sseq12d 
 |-  ( x = 1 -> ( U_ k e. NN ( ( D ^r k ) ^r x ) C_ ( U_ j e. NN ( D ^r j ) ^r x ) <-> U_ k e. NN ( ( D ^r k ) ^r 1 ) C_ ( U_ j e. NN ( D ^r j ) ^r 1 ) ) )
5 oveq2 
 |-  ( x = y -> ( ( D ^r k ) ^r x ) = ( ( D ^r k ) ^r y ) )
6 5 iuneq2d 
 |-  ( x = y -> U_ k e. NN ( ( D ^r k ) ^r x ) = U_ k e. NN ( ( D ^r k ) ^r y ) )
7 oveq2 
 |-  ( x = y -> ( U_ j e. NN ( D ^r j ) ^r x ) = ( U_ j e. NN ( D ^r j ) ^r y ) )
8 6 7 sseq12d 
 |-  ( x = y -> ( U_ k e. NN ( ( D ^r k ) ^r x ) C_ ( U_ j e. NN ( D ^r j ) ^r x ) <-> U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) ) )
9 oveq2 
 |-  ( x = ( y + 1 ) -> ( ( D ^r k ) ^r x ) = ( ( D ^r k ) ^r ( y + 1 ) ) )
10 9 iuneq2d 
 |-  ( x = ( y + 1 ) -> U_ k e. NN ( ( D ^r k ) ^r x ) = U_ k e. NN ( ( D ^r k ) ^r ( y + 1 ) ) )
11 oveq2 
 |-  ( x = ( y + 1 ) -> ( U_ j e. NN ( D ^r j ) ^r x ) = ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) )
12 10 11 sseq12d 
 |-  ( x = ( y + 1 ) -> ( U_ k e. NN ( ( D ^r k ) ^r x ) C_ ( U_ j e. NN ( D ^r j ) ^r x ) <-> U_ k e. NN ( ( D ^r k ) ^r ( y + 1 ) ) C_ ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) ) )
13 oveq2 
 |-  ( x = N -> ( ( D ^r k ) ^r x ) = ( ( D ^r k ) ^r N ) )
14 13 iuneq2d 
 |-  ( x = N -> U_ k e. NN ( ( D ^r k ) ^r x ) = U_ k e. NN ( ( D ^r k ) ^r N ) )
15 oveq2 
 |-  ( x = N -> ( U_ j e. NN ( D ^r j ) ^r x ) = ( U_ j e. NN ( D ^r j ) ^r N ) )
16 14 15 sseq12d 
 |-  ( x = N -> ( U_ k e. NN ( ( D ^r k ) ^r x ) C_ ( U_ j e. NN ( D ^r j ) ^r x ) <-> U_ k e. NN ( ( D ^r k ) ^r N ) C_ ( U_ j e. NN ( D ^r j ) ^r N ) ) )
17 oveq2 
 |-  ( k = l -> ( D ^r k ) = ( D ^r l ) )
18 17 cbviunv 
 |-  U_ k e. NN ( D ^r k ) = U_ l e. NN ( D ^r l )
19 oveq2 
 |-  ( l = j -> ( D ^r l ) = ( D ^r j ) )
20 19 cbviunv 
 |-  U_ l e. NN ( D ^r l ) = U_ j e. NN ( D ^r j )
21 18 20 eqtri 
 |-  U_ k e. NN ( D ^r k ) = U_ j e. NN ( D ^r j )
22 ovex 
 |-  ( D ^r k ) e. _V
23 relexp1g 
 |-  ( ( D ^r k ) e. _V -> ( ( D ^r k ) ^r 1 ) = ( D ^r k ) )
24 22 23 mp1i 
 |-  ( k e. NN -> ( ( D ^r k ) ^r 1 ) = ( D ^r k ) )
25 24 iuneq2i 
 |-  U_ k e. NN ( ( D ^r k ) ^r 1 ) = U_ k e. NN ( D ^r k )
26 nnex 
 |-  NN e. _V
27 ovex 
 |-  ( D ^r j ) e. _V
28 26 27 iunex 
 |-  U_ j e. NN ( D ^r j ) e. _V
29 relexp1g 
 |-  ( U_ j e. NN ( D ^r j ) e. _V -> ( U_ j e. NN ( D ^r j ) ^r 1 ) = U_ j e. NN ( D ^r j ) )
30 28 29 ax-mp 
 |-  ( U_ j e. NN ( D ^r j ) ^r 1 ) = U_ j e. NN ( D ^r j )
31 21 25 30 3eqtr4i 
 |-  U_ k e. NN ( ( D ^r k ) ^r 1 ) = ( U_ j e. NN ( D ^r j ) ^r 1 )
32 31 eqimssi 
 |-  U_ k e. NN ( ( D ^r k ) ^r 1 ) C_ ( U_ j e. NN ( D ^r j ) ^r 1 )
33 oveq2 
 |-  ( k = m -> ( D ^r k ) = ( D ^r m ) )
34 33 oveq1d 
 |-  ( k = m -> ( ( D ^r k ) ^r y ) = ( ( D ^r m ) ^r y ) )
35 34 33 coeq12d 
 |-  ( k = m -> ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) = ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) ) )
36 35 cbviunv 
 |-  U_ k e. NN ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) = U_ m e. NN ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) )
37 ss2iun 
 |-  ( A. m e. NN ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) ) C_ ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) -> U_ m e. NN ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) ) C_ U_ m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) )
38 34 ssiun2s 
 |-  ( m e. NN -> ( ( D ^r m ) ^r y ) C_ U_ k e. NN ( ( D ^r k ) ^r y ) )
39 coss1 
 |-  ( ( ( D ^r m ) ^r y ) C_ U_ k e. NN ( ( D ^r k ) ^r y ) -> ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) ) C_ ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) )
40 38 39 syl 
 |-  ( m e. NN -> ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) ) C_ ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) )
41 37 40 mprg 
 |-  U_ m e. NN ( ( ( D ^r m ) ^r y ) o. ( D ^r m ) ) C_ U_ m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) )
42 36 41 eqsstri 
 |-  U_ k e. NN ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) C_ U_ m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) )
43 coss1 
 |-  ( U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) -> ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) C_ ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
44 43 ralrimivw 
 |-  ( U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) -> A. m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) C_ ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
45 ss2iun 
 |-  ( A. m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) C_ ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) -> U_ m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) C_ U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
46 44 45 syl 
 |-  ( U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) -> U_ m e. NN ( U_ k e. NN ( ( D ^r k ) ^r y ) o. ( D ^r m ) ) C_ U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
47 42 46 sstrid 
 |-  ( U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) -> U_ k e. NN ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) C_ U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
48 47 adantl 
 |-  ( ( y e. NN /\ U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) ) -> U_ k e. NN ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) C_ U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
49 relexpsucnnr 
 |-  ( ( ( D ^r k ) e. _V /\ y e. NN ) -> ( ( D ^r k ) ^r ( y + 1 ) ) = ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) )
50 22 49 mpan 
 |-  ( y e. NN -> ( ( D ^r k ) ^r ( y + 1 ) ) = ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) )
51 50 iuneq2d 
 |-  ( y e. NN -> U_ k e. NN ( ( D ^r k ) ^r ( y + 1 ) ) = U_ k e. NN ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) )
52 51 adantr 
 |-  ( ( y e. NN /\ U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) ) -> U_ k e. NN ( ( D ^r k ) ^r ( y + 1 ) ) = U_ k e. NN ( ( ( D ^r k ) ^r y ) o. ( D ^r k ) ) )
53 relexpsucnnr 
 |-  ( ( U_ j e. NN ( D ^r j ) e. _V /\ y e. NN ) -> ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) = ( ( U_ j e. NN ( D ^r j ) ^r y ) o. U_ j e. NN ( D ^r j ) ) )
54 28 53 mpan 
 |-  ( y e. NN -> ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) = ( ( U_ j e. NN ( D ^r j ) ^r y ) o. U_ j e. NN ( D ^r j ) ) )
55 oveq2 
 |-  ( j = m -> ( D ^r j ) = ( D ^r m ) )
56 55 cbviunv 
 |-  U_ j e. NN ( D ^r j ) = U_ m e. NN ( D ^r m )
57 56 coeq2i 
 |-  ( ( U_ j e. NN ( D ^r j ) ^r y ) o. U_ j e. NN ( D ^r j ) ) = ( ( U_ j e. NN ( D ^r j ) ^r y ) o. U_ m e. NN ( D ^r m ) )
58 coiun 
 |-  ( ( U_ j e. NN ( D ^r j ) ^r y ) o. U_ m e. NN ( D ^r m ) ) = U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) )
59 57 58 eqtri 
 |-  ( ( U_ j e. NN ( D ^r j ) ^r y ) o. U_ j e. NN ( D ^r j ) ) = U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) )
60 54 59 eqtrdi 
 |-  ( y e. NN -> ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) = U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
61 60 adantr 
 |-  ( ( y e. NN /\ U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) ) -> ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) = U_ m e. NN ( ( U_ j e. NN ( D ^r j ) ^r y ) o. ( D ^r m ) ) )
62 48 52 61 3sstr4d 
 |-  ( ( y e. NN /\ U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) ) -> U_ k e. NN ( ( D ^r k ) ^r ( y + 1 ) ) C_ ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) )
63 62 ex 
 |-  ( y e. NN -> ( U_ k e. NN ( ( D ^r k ) ^r y ) C_ ( U_ j e. NN ( D ^r j ) ^r y ) -> U_ k e. NN ( ( D ^r k ) ^r ( y + 1 ) ) C_ ( U_ j e. NN ( D ^r j ) ^r ( y + 1 ) ) ) )
64 4 8 12 16 32 63 nnind 
 |-  ( N e. NN -> U_ k e. NN ( ( D ^r k ) ^r N ) C_ ( U_ j e. NN ( D ^r j ) ^r N ) )