Metamath Proof Explorer

Theorem relexp1idm

Description: Repeated raising a relation to the first power is idempotent. (Contributed by RP, 12-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 ifid 
 |-  if ( 1 < 1 , 1 , 1 ) = 1
2 1 eqcomi 
 |-  1 = if ( 1 < 1 , 1 , 1 )
3 2 jctr 
 |-  ( R e. V -> ( R e. V /\ 1 = if ( 1 < 1 , 1 , 1 ) ) )
4 1ex 
 |-  1 e. _V
5 4 prid2 
 |-  1 e. { 0 , 1 }
6 5 5 pm3.2i 
 |-  ( 1 e. { 0 , 1 } /\ 1 e. { 0 , 1 } )
7 relexp01min 
 |-  ( ( ( R e. V /\ 1 = if ( 1 < 1 , 1 , 1 ) ) /\ ( 1 e. { 0 , 1 } /\ 1 e. { 0 , 1 } ) ) -> ( ( R ^r 1 ) ^r 1 ) = ( R ^r 1 ) )
8 3 6 7 sylancl 
 |-  ( R e. V -> ( ( R ^r 1 ) ^r 1 ) = ( R ^r 1 ) )