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 bilani 
 |-  ( ( R e. V /\ N e. NN ) -> N e. ( ZZ>= ` 1 ) )
47 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 ) ) ) )
48 46 47 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 ) ) ) )
49 ovex 
 |-  ( N + 1 ) e. _V
50 simpl 
 |-  ( ( R e. V /\ N e. NN ) -> R e. V )
51 eqidd 
 |-  ( z = ( N + 1 ) -> R = R )
52 eqid 
 |-  ( z e. _V |-> R ) = ( z e. _V |-> R )
53 51 52 fvmptg 
 |-  ( ( ( N + 1 ) e. _V /\ R e. V ) -> ( ( z e. _V |-> R ) ` ( N + 1 ) ) = R )
54 49 50 53 sylancr 
 |-  ( ( R e. V /\ N e. NN ) -> ( ( z e. _V |-> R ) ` ( N + 1 ) ) = R )
55 54 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 ) )
56 nfcv 
 |-  F/_ a ( x o. R )
57 nfcv 
 |-  F/_ b ( x o. R )
58 nfcv 
 |-  F/_ x ( a o. R )
59 nfcv 
 |-  F/_ y ( a o. R )
60 simpl 
 |-  ( ( x = a /\ y = b ) -> x = a )
61 60 coeq1d 
 |-  ( ( x = a /\ y = b ) -> ( x o. R ) = ( a o. R ) )
62 56 57 58 59 61 cbvmpo 
 |-  ( x e. _V , y e. _V |-> ( x o. R ) ) = ( a e. _V , b e. _V |-> ( a o. R ) )
63 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 ) )
64 62 63 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 ) )
65 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 ) ) )
66 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 ) )
67 66 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 ) )
68 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 )
69 fvex 
 |-  ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. R ) ) , ( z e. _V |-> R ) ) ` N ) e. _V
70 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 )
71 69 50 70 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 )
72 65 67 68 27 71 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 ) )
73 simpr 
 |-  ( ( r = R /\ n = N ) -> n = N )
74 73 eqeq1d 
 |-  ( ( r = R /\ n = N ) -> ( n = 0 <-> N = 0 ) )
75 6 adantr 
 |-  ( ( r = R /\ n = N ) -> ( _I |` ( dom r u. ran r ) ) = ( _I |` ( dom R u. ran R ) ) )
76 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 ) ) )
77 76 73 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 ) )
78 74 75 77 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 ) ) )
79 78 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 ) ) )
80 28 nnnn0d 
 |-  ( ( R e. V /\ N e. NN ) -> N e. NN0 )
81 37 68 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 )
82 1 79 27 80 81 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 ) ) )
83 nnne0 
 |-  ( N e. NN -> N =/= 0 )
84 83 adantl 
 |-  ( ( R e. V /\ N e. NN ) -> N =/= 0 )
85 84 neneqd 
 |-  ( ( R e. V /\ N e. NN ) -> -. N = 0 )
86 85 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 ) )
87 82 86 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 ) )
88 87 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 ) )
89 64 72 88 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 ) )
90 48 55 89 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 ) )
91 40 44 90 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 ) )
92 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 ) ) )
93 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 ) ) )
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 ) = ( 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 ) )
95 94 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 ) )
96 93 95 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 ) ) )
97 96 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 ) ) ) )
98 92 97 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 ) ) )
99 91 98 mpbir 
 |-  ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )