Metamath Proof Explorer

Theorem relexp1g

Description: A relation composed once is itself. (Contributed by RP, 22-May-2020)

Ref Expression
Assertion relexp1g 
|- ( R e. V -> ( R ^r 1 ) = R )

Proof

Step Hyp Ref Expression
1 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 ) ) )
2 1 a1i 
 |-  ( R e. V -> ^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 ) ) ) )
3 simprr 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> n = 1 )
4 ax-1ne0 
 |-  1 =/= 0
5 neeq1 
 |-  ( n = 1 -> ( n =/= 0 <-> 1 =/= 0 ) )
6 4 5 mpbiri 
 |-  ( n = 1 -> n =/= 0 )
7 3 6 syl 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> n =/= 0 )
8 7 neneqd 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> -. n = 0 )
9 8 iffalsed 
 |-  ( ( R e. V /\ ( r = R /\ 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 ) ) = ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) )
10 simprl 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> r = R )
11 10 mpteq2dv 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> ( z e. _V |-> r ) = ( z e. _V |-> R ) )
12 11 seqeq3d 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> 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 3 fveq12d 
 |-  ( ( R e. V /\ ( r = R /\ 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 ) ) ` 1 ) )
14 1z 
 |-  1 e. ZZ
15 eqidd 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> ( z e. _V |-> R ) = ( z e. _V |-> R ) )
16 eqidd 
 |-  ( ( ( R e. V /\ ( r = R /\ n = 1 ) ) /\ z = 1 ) -> R = R )
17 1ex 
 |-  1 e. _V
18 17 a1i 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> 1 e. _V )
19 simpl 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> R e. V )
20 15 16 18 19 fvmptd 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> ( ( z e. _V |-> R ) ` 1 ) = R )
21 14 20 seq1i 
 |-  ( ( R e. V /\ ( r = R /\ n = 1 ) ) -> ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> R ) ) ` 1 ) = R )
22 9 13 21 3eqtrd 
 |-  ( ( R e. V /\ ( r = R /\ 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 ) ) = R )
23 elex 
 |-  ( R e. V -> R e. _V )
24 1nn0 
 |-  1 e. NN0
25 24 a1i 
 |-  ( R e. V -> 1 e. NN0 )
26 2 22 23 25 23 ovmpod 
 |-  ( R e. V -> ( R ^r 1 ) = R )