Metamath Proof Explorer

Theorem relexp0idm

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

Ref Expression
Assertion relexp0idm 
|- ( R e. V -> ( ( R ^r 0 ) ^r 0 ) = ( R ^r 0 ) )

Proof

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