Metamath Proof Explorer

Theorem relexpsucnnr

Description: A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020)

Ref Expression
Assertion relexpsucnnr 
|- ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( ( R e. V /\ N e. NN ) -> ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) )
2 simprr 
 |-  ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ n = ( N + 1 ) ) ) -> n = ( N + 1 ) )
3 dmeq 
 |-  ( r = R -> dom r = dom R )
4 rneq 
 |-  ( r = R -> ran r = ran R )
5 3 4 uneq12d 
 |-  ( r = R -> ( dom r u. ran r ) = ( dom R u. ran R ) )
6 5 reseq2d 
 |-  ( r = R -> ( _I |` ( dom r u. ran r ) ) = ( _I |` ( dom R u. ran R ) ) )
7 eqidd 
 |-  ( r = R -> 1 = 1 )
8 coeq2 
 |-  ( r = R -> ( x o. r ) = ( x o. R ) )
9 8 mpoeq3dv 
 |-  ( r = R -> ( x e. _V , y e. _V |-> ( x o. r ) ) = ( x e. _V , y e. _V |-> ( x o. R ) ) )
10 id 
 |-  ( r = R -> r = R )
11 10 mpteq2dv 
 |-  ( r = R -> ( z e. _V |-> r ) = ( z e. _V |-> R ) )
12 7 9 11 seqeq123d 
 |-  ( r = R -> seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) = seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) )
13 12 fveq1d 
 |-  ( r = R -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) )
14 6 13 ifeq12d 
 |-  ( r = R -> if ( ( N + 1 ) = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) )
15 14 ad2antrl 
 |-  ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ ( N + 1 ) = ( N + 1 ) ) ) -> if ( ( N + 1 ) = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) )
16 15 a1i 
 |-  ( n = ( N + 1 ) -> ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ ( N + 1 ) = ( N + 1 ) ) ) -> if ( ( N + 1 ) = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) ) )
17 eqeq1 
 |-  ( n = ( N + 1 ) -> ( n = ( N + 1 ) <-> ( N + 1 ) = ( N + 1 ) ) )
18 17 anbi2d 
 |-  ( n = ( N + 1 ) -> ( ( r = R /\ n = ( N + 1 ) ) <-> ( r = R /\ ( N + 1 ) = ( N + 1 ) ) ) )
19 18 anbi2d 
 |-  ( n = ( N + 1 ) -> ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ n = ( N + 1 ) ) ) <-> ( ( R e. V /\ N e. NN ) /\ ( r = R /\ ( N + 1 ) = ( N + 1 ) ) ) ) )
20 eqeq1 
 |-  ( n = ( N + 1 ) -> ( n = 0 <-> ( N + 1 ) = 0 ) )
21 fveq2 
 |-  ( n = ( N + 1 ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) )
22 20 21 ifbieq2d 
 |-  ( n = ( N + 1 ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) ) )
23 22 eqeq1d 
 |-  ( n = ( N + 1 ) -> ( if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) <-> if ( ( N + 1 ) = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` ( N + 1 ) ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) ) )
24 16 19 23 3imtr4d 
 |-  ( n = ( N + 1 ) -> ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ n = ( N + 1 ) ) ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) ) )
25 2 24 mpcom 
 |-  ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ n = ( N + 1 ) ) ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) )
26 elex 
 |-  ( R e. V -> R e. _V )
27 26 adantr 
 |-  ( ( R e. V /\ N e. NN ) -> R e. _V )
28 simpr 
 |-  ( ( R e. V /\ N e. NN ) -> N e. NN )
29 28 peano2nnd 
 |-  ( ( R e. V /\ N e. NN ) -> ( N + 1 ) e. NN )
30 29 nnnn0d 
 |-  ( ( R e. V /\ N e. NN ) -> ( N + 1 ) e. NN0 )
31 dmexg 
 |-  ( R e. V -> dom R e. _V )
32 rnexg 
 |-  ( R e. V -> ran R e. _V )
33 unexg 
 |-  ( ( dom R e. _V /\ ran R e. _V ) -> ( dom R u. ran R ) e. _V )
34 31 32 33 syl2anc 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
35 resiexg 
 |-  ( ( dom R u. ran R ) e. _V -> ( _I |` ( dom R u. ran R ) ) e. _V )
36 34 35 syl 
 |-  ( R e. V -> ( _I |` ( dom R u. ran R ) ) e. _V )
37 36 adantr 
 |-  ( ( R e. V /\ N e. NN ) -> ( _I |` ( dom R u. ran R ) ) e. _V )
38 fvexd 
 |-  ( ( R e. V /\ N e. NN ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) e. _V )
39 37 38 ifcld 
 |-  ( ( R e. V /\ N e. NN ) -> if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) e. _V )
40 1 25 27 30 39 ovmpod 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) ( N + 1 ) ) = if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) )
41 nnne0 
 |-  ( ( N + 1 ) e. NN -> ( N + 1 ) =/= 0 )
42 41 neneqd 
 |-  ( ( N + 1 ) e. NN -> -. ( N + 1 ) = 0 )
43 29 42 syl 
 |-  ( ( R e. V /\ N e. NN ) -> -. ( N + 1 ) = 0 )
44 43 iffalsed 
 |-  ( ( R e. V /\ N e. NN ) -> if ( ( N + 1 ) = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) ) = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) )
45 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
46 45 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
47 46 adantl 
 |-  ( ( R e. V /\ N e. NN ) -> N e. ( ZZ>= ` 1 ) )
48 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) ( ( z e. _V |-> R ) ` ( N + 1 ) ) ) )
49 47 48 syl 
 |-  ( ( R e. V /\ N e. NN ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) ( ( z e. _V |-> R ) ` ( N + 1 ) ) ) )
50 ovex 
 |-  ( N + 1 ) e. _V
51 simpl 
 |-  ( ( R e. V /\ N e. NN ) -> R e. V )
52 eqidd 
 |-  ( z = ( N + 1 ) -> R = R )
53 eqid 
 |-  ( z e. _V |-> R ) = ( z e. _V |-> R )
54 52 53 fvmptg 
 |-  ( ( ( N + 1 ) e. _V /\ R e. V ) -> ( ( z e. _V |-> R ) ` ( N + 1 ) ) = R )
55 50 51 54 sylancr 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( z e. _V |-> R ) ` ( N + 1 ) ) = R )
56 55 oveq2d 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) ( ( z e. _V |-> R ) ` ( N + 1 ) ) ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) R ) )
57 nfcv 
 |-  F/_ a ( x o. R )
58 nfcv 
 |-  F/_ b ( x o. R )
59 nfcv 
 |-  F/_ x ( a o. R )
60 nfcv 
 |-  F/_ y ( a o. R )
61 simpl 
 |-  ( ( x = a /\ y = b ) -> x = a )
62 61 coeq1d 
 |-  ( ( x = a /\ y = b ) -> ( x o. R ) = ( a o. R ) )
63 57 58 59 60 62 cbvmpo 
 |-  ( x e. _V , y e. _V |-> ( x o. R ) ) = ( a e. _V , b e. _V |-> ( a o. R ) )
64 oveq 
 |-  ( ( x e. _V , y e. _V |-> ( x o. R ) ) = ( a e. _V , b e. _V |-> ( a o. R ) ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) R ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( a e. _V , b e. _V |-> ( a o. R ) ) R ) )
65 63 64 mp1i 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) R ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( a e. _V , b e. _V |-> ( a o. R ) ) R ) )
66 eqidd 
 |-  ( ( R e. V /\ N e. NN ) -> ( a e. _V , b e. _V |-> ( a o. R ) ) = ( a e. _V , b e. _V |-> ( a o. R ) ) )
67 simprl 
 |-  ( ( ( R e. V /\ N e. NN ) /\ ( a = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) /\ b = R ) ) -> a = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) )
68 67 coeq1d 
 |-  ( ( ( R e. V /\ N e. NN ) /\ ( a = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) /\ b = R ) ) -> ( a o. R ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) o. R ) )
69 fvexd 
 |-  ( ( R e. V /\ N e. NN ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) e. _V )
70 fvex 
 |-  ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) e. _V
71 coexg 
 |-  ( ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) e. _V /\ R e. V ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) o. R ) e. _V )
72 70 51 71 sylancr 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) o. R ) e. _V )
73 66 68 69 27 72 ovmpod 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( a e. _V , b e. _V |-> ( a o. R ) ) R ) = ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) o. R ) )
74 simpr 
 |-  ( ( r = R /\ n = N ) -> n = N )
75 74 eqeq1d 
 |-  ( ( r = R /\ n = N ) -> ( n = 0 <-> N = 0 ) )
76 6 adantr 
 |-  ( ( r = R /\ n = N ) -> ( _I |` ( dom r u. ran r ) ) = ( _I |` ( dom R u. ran R ) ) )
77 12 adantr 
 |-  ( ( r = R /\ n = N ) -> seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) = seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) )
78 77 74 fveq12d 
 |-  ( ( r = R /\ n = N ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) )
79 75 76 78 ifbieq12d 
 |-  ( ( r = R /\ n = N ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = if ( N = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ) )
80 79 adantl 
 |-  ( ( ( R e. V /\ N e. NN ) /\ ( r = R /\ n = N ) ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = if ( N = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ) )
81 28 nnnn0d 
 |-  ( ( R e. V /\ N e. NN ) -> N e. NN0 )
82 37 69 ifcld 
 |-  ( ( R e. V /\ N e. NN ) -> if ( N = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ) e. _V )
83 1 80 27 81 82 ovmpod 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) = if ( N = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ) )
84 nnne0 
 |-  ( N e. NN -> N =/= 0 )
85 84 adantl 
 |-  ( ( R e. V /\ N e. NN ) -> N =/= 0 )
86 85 neneqd 
 |-  ( ( R e. V /\ N e. NN ) -> -. N = 0 )
87 86 iffalsed 
 |-  ( ( R e. V /\ N e. NN ) -> if ( N = 0 , ( _I |` ( dom R u. ran R ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ) = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) )
88 83 87 eqtr2d 
 |-  ( ( R e. V /\ N e. NN ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) = ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) )
89 88 coeq1d 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) o. R ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) )
90 65 73 89 3eqtrd 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) ( x e. _V , y e. _V |-> ( x o. R ) ) R ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) )
91 49 56 90 3eqtrd 
 |-  ( ( R e. V /\ N e. NN ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` ( N + 1 ) ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) )
92 40 44 91 3eqtrd 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) ( N + 1 ) ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) )
93 df-relexp 
 |-  ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )
94 oveq 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( R ^r ( N + 1 ) ) = ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) ( N + 1 ) ) )
95 oveq 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( R ^r N ) = ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) )
96 95 coeq1d 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( ( R ^r N ) o. R ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) )
97 94 96 eqeq12d 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) <-> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) ( N + 1 ) ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) ) )
98 97 imbi2d 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) <-> ( ( R e. V /\ N e. NN ) -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) ( N + 1 ) ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) ) ) )
99 93 98 ax-mp 
 |-  ( ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) <-> ( ( R e. V /\ N e. NN ) -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) ( N + 1 ) ) = ( ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) N ) o. R ) ) )
100 92 99 mpbir 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )