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 ( 𝑅𝑉 → ( ( 𝑅𝑟 0 ) ↑𝑟 0 ) = ( 𝑅𝑟 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 ( 𝑅𝑉 → ( 𝑅𝑉 ∧ 0 = if ( 0 < 0 , 0 , 0 ) ) )
4 c0ex 0 ∈ V
5 4 prid1 0 ∈ { 0 , 1 }
6 5 5 pm3.2i ( 0 ∈ { 0 , 1 } ∧ 0 ∈ { 0 , 1 } )
7 relexp01min ( ( ( 𝑅𝑉 ∧ 0 = if ( 0 < 0 , 0 , 0 ) ) ∧ ( 0 ∈ { 0 , 1 } ∧ 0 ∈ { 0 , 1 } ) ) → ( ( 𝑅𝑟 0 ) ↑𝑟 0 ) = ( 𝑅𝑟 0 ) )
8 3 6 7 sylancl ( 𝑅𝑉 → ( ( 𝑅𝑟 0 ) ↑𝑟 0 ) = ( 𝑅𝑟 0 ) )