Metamath Proof Explorer

Theorem relexp0g

Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020)

Ref Expression
Assertion relexp0g ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) )
2 simprr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 0 ) ) → 𝑛 = 0 )
3 2 iftrued ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 0 ) ) → if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) = ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) )
4 dmeq ⊢ ( 𝑟 = 𝑅 → dom 𝑟 = dom 𝑅 )
5 rneq ⊢ ( 𝑟 = 𝑅 → ran 𝑟 = ran 𝑅 )
6 4 5 uneq12d ⊢ ( 𝑟 = 𝑅 → ( dom 𝑟 ∪ ran 𝑟 ) = ( dom 𝑅 ∪ ran 𝑅 ) )
7 6 reseq2d ⊢ ( 𝑟 = 𝑅 → ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
8 7 ad2antrl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 0 ) ) → ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
9 3 8 eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 0 ) ) → if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
10 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
11 0nn0 ⊢ 0 ∈ ℕ0
12 11 a1i ⊢ ( 𝑅 ∈ 𝑉 → 0 ∈ ℕ0 )
13 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
14 rnexg ⊢ ( 𝑅 ∈ 𝑉 → ran 𝑅 ∈ V )
15 unexg ⊢ ( ( dom 𝑅 ∈ V ∧ ran 𝑅 ∈ V ) → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
16 13 14 15 syl2anc ⊢ ( 𝑅 ∈ 𝑉 → ( dom 𝑅 ∪ ran 𝑅 ) ∈ V )
17 resiexg ⊢ ( ( dom 𝑅 ∪ ran 𝑅 ) ∈ V → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
18 16 17 syl ⊢ ( 𝑅 ∈ 𝑉 → ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ∈ V )
19 1 9 10 12 18 ovmpod ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
20 df-relexp ⊢ ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )
21 oveq ⊢ ( ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) → ( 𝑅 ↑𝑟 0 ) = ( 𝑅 ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) 0 ) )
22 21 eqeq1d ⊢ ( ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) → ( ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ↔ ( 𝑅 ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
23 22 imbi2d ⊢ ( ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) → ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( 𝑅 ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ) )
24 20 23 ax-mp ⊢ ( ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) ↔ ( 𝑅 ∈ 𝑉 → ( 𝑅 ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
25 19 24 mpbir ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )