Metamath Proof Explorer

Theorem relexprelg

Description: The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020)

Ref Expression
Assertion relexprelg 
|- ( ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 eqeq1 
 |-  ( n = 1 -> ( n = 1 <-> 1 = 1 ) )
3 2 imbi1d 
 |-  ( n = 1 -> ( ( n = 1 -> Rel R ) <-> ( 1 = 1 -> Rel R ) ) )
4 3 anbi2d 
 |-  ( n = 1 -> ( ( R e. V /\ ( n = 1 -> Rel R ) ) <-> ( R e. V /\ ( 1 = 1 -> Rel R ) ) ) )
5 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
6 5 releqd 
 |-  ( n = 1 -> ( Rel ( R ^r n ) <-> Rel ( R ^r 1 ) ) )
7 4 6 imbi12d 
 |-  ( n = 1 -> ( ( ( R e. V /\ ( n = 1 -> Rel R ) ) -> Rel ( R ^r n ) ) <-> ( ( R e. V /\ ( 1 = 1 -> Rel R ) ) -> Rel ( R ^r 1 ) ) ) )
8 eqeq1 
 |-  ( n = m -> ( n = 1 <-> m = 1 ) )
9 8 imbi1d 
 |-  ( n = m -> ( ( n = 1 -> Rel R ) <-> ( m = 1 -> Rel R ) ) )
10 9 anbi2d 
 |-  ( n = m -> ( ( R e. V /\ ( n = 1 -> Rel R ) ) <-> ( R e. V /\ ( m = 1 -> Rel R ) ) ) )
11 oveq2 
 |-  ( n = m -> ( R ^r n ) = ( R ^r m ) )
12 11 releqd 
 |-  ( n = m -> ( Rel ( R ^r n ) <-> Rel ( R ^r m ) ) )
13 10 12 imbi12d 
 |-  ( n = m -> ( ( ( R e. V /\ ( n = 1 -> Rel R ) ) -> Rel ( R ^r n ) ) <-> ( ( R e. V /\ ( m = 1 -> Rel R ) ) -> Rel ( R ^r m ) ) ) )
14 eqeq1 
 |-  ( n = ( m + 1 ) -> ( n = 1 <-> ( m + 1 ) = 1 ) )
15 14 imbi1d 
 |-  ( n = ( m + 1 ) -> ( ( n = 1 -> Rel R ) <-> ( ( m + 1 ) = 1 -> Rel R ) ) )
16 15 anbi2d 
 |-  ( n = ( m + 1 ) -> ( ( R e. V /\ ( n = 1 -> Rel R ) ) <-> ( R e. V /\ ( ( m + 1 ) = 1 -> Rel R ) ) ) )
17 oveq2 
 |-  ( n = ( m + 1 ) -> ( R ^r n ) = ( R ^r ( m + 1 ) ) )
18 17 releqd 
 |-  ( n = ( m + 1 ) -> ( Rel ( R ^r n ) <-> Rel ( R ^r ( m + 1 ) ) ) )
19 16 18 imbi12d 
 |-  ( n = ( m + 1 ) -> ( ( ( R e. V /\ ( n = 1 -> Rel R ) ) -> Rel ( R ^r n ) ) <-> ( ( R e. V /\ ( ( m + 1 ) = 1 -> Rel R ) ) -> Rel ( R ^r ( m + 1 ) ) ) ) )
20 eqeq1 
 |-  ( n = N -> ( n = 1 <-> N = 1 ) )
21 20 imbi1d 
 |-  ( n = N -> ( ( n = 1 -> Rel R ) <-> ( N = 1 -> Rel R ) ) )
22 21 anbi2d 
 |-  ( n = N -> ( ( R e. V /\ ( n = 1 -> Rel R ) ) <-> ( R e. V /\ ( N = 1 -> Rel R ) ) ) )
23 oveq2 
 |-  ( n = N -> ( R ^r n ) = ( R ^r N ) )
24 23 releqd 
 |-  ( n = N -> ( Rel ( R ^r n ) <-> Rel ( R ^r N ) ) )
25 22 24 imbi12d 
 |-  ( n = N -> ( ( ( R e. V /\ ( n = 1 -> Rel R ) ) -> Rel ( R ^r n ) ) <-> ( ( R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) ) ) )
26 eqid 
 |-  1 = 1
27 pm2.27 
 |-  ( 1 = 1 -> ( ( 1 = 1 -> Rel R ) -> Rel R ) )
28 26 27 ax-mp 
 |-  ( ( 1 = 1 -> Rel R ) -> Rel R )
29 28 adantl 
 |-  ( ( R e. V /\ ( 1 = 1 -> Rel R ) ) -> Rel R )
30 relexp1g 
 |-  ( R e. V -> ( R ^r 1 ) = R )
31 30 adantr 
 |-  ( ( R e. V /\ ( 1 = 1 -> Rel R ) ) -> ( R ^r 1 ) = R )
32 31 releqd 
 |-  ( ( R e. V /\ ( 1 = 1 -> Rel R ) ) -> ( Rel ( R ^r 1 ) <-> Rel R ) )
33 29 32 mpbird 
 |-  ( ( R e. V /\ ( 1 = 1 -> Rel R ) ) -> Rel ( R ^r 1 ) )
34 relco 
 |-  Rel ( ( R ^r m ) o. R )
35 relexpsucnnr 
 |-  ( ( R e. V /\ m e. NN ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
36 35 ancoms 
 |-  ( ( m e. NN /\ R e. V ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
37 36 releqd 
 |-  ( ( m e. NN /\ R e. V ) -> ( Rel ( R ^r ( m + 1 ) ) <-> Rel ( ( R ^r m ) o. R ) ) )
38 34 37 mpbiri 
 |-  ( ( m e. NN /\ R e. V ) -> Rel ( R ^r ( m + 1 ) ) )
39 38 a1d 
 |-  ( ( m e. NN /\ R e. V ) -> ( ( ( m + 1 ) = 1 -> Rel R ) -> Rel ( R ^r ( m + 1 ) ) ) )
40 39 expimpd 
 |-  ( m e. NN -> ( ( R e. V /\ ( ( m + 1 ) = 1 -> Rel R ) ) -> Rel ( R ^r ( m + 1 ) ) ) )
41 40 a1d 
 |-  ( m e. NN -> ( ( ( R e. V /\ ( m = 1 -> Rel R ) ) -> Rel ( R ^r m ) ) -> ( ( R e. V /\ ( ( m + 1 ) = 1 -> Rel R ) ) -> Rel ( R ^r ( m + 1 ) ) ) ) )
42 7 13 19 25 33 41 nnind 
 |-  ( N e. NN -> ( ( R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) ) )
43 relexp0rel 
 |-  ( R e. V -> Rel ( R ^r 0 ) )
44 43 adantl 
 |-  ( ( N = 0 /\ R e. V ) -> Rel ( R ^r 0 ) )
45 simpl 
 |-  ( ( N = 0 /\ R e. V ) -> N = 0 )
46 45 oveq2d 
 |-  ( ( N = 0 /\ R e. V ) -> ( R ^r N ) = ( R ^r 0 ) )
47 46 releqd 
 |-  ( ( N = 0 /\ R e. V ) -> ( Rel ( R ^r N ) <-> Rel ( R ^r 0 ) ) )
48 44 47 mpbird 
 |-  ( ( N = 0 /\ R e. V ) -> Rel ( R ^r N ) )
49 48 a1d 
 |-  ( ( N = 0 /\ R e. V ) -> ( ( N = 1 -> Rel R ) -> Rel ( R ^r N ) ) )
50 49 expimpd 
 |-  ( N = 0 -> ( ( R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) ) )
51 42 50 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( ( R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) ) )
52 1 51 sylbi 
 |-  ( N e. NN0 -> ( ( R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) ) )
53 52 3impib 
 |-  ( ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) )