Description: Repeated raising a relation to the zeroth power is idempotent. (Contributed by RP, 12-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | relexp0idm | ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 ↑𝑟 0 ) ↑𝑟 0 ) = ( 𝑅 ↑𝑟 0 ) ) |
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 ) ) |