Metamath Proof Explorer

Theorem relexp1g

Description: A relation composed once is itself. (Contributed by RP, 22-May-2020)

Ref Expression
Assertion relexp1g ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 df-relexp ⊢ ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) )
2 1 a1i ⊢ ( 𝑅 ∈ 𝑉 → ↑𝑟 = ( 𝑟 ∈ V , 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) ) )
3 simprr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → 𝑛 = 1 )
4 ax-1ne0 ⊢ 1 ≠ 0
5 neeq1 ⊢ ( 𝑛 = 1 → ( 𝑛 ≠ 0 ↔ 1 ≠ 0 ) )
6 4 5 mpbiri ⊢ ( 𝑛 = 1 → 𝑛 ≠ 0 )
7 3 6 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → 𝑛 ≠ 0 )
8 7 neneqd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → ¬ 𝑛 = 0 )
9 8 iffalsed ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) = ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) )
10 simprl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → 𝑟 = 𝑅 )
11 10 mpteq2dv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → ( 𝑧 ∈ V ↦ 𝑟 ) = ( 𝑧 ∈ V ↦ 𝑅 ) )
12 11 seqeq3d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) = seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑅 ) ) )
13 12 3 fveq12d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) = ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑅 ) ) ‘ 1 ) )
14 1z ⊢ 1 ∈ ℤ
15 eqidd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → ( 𝑧 ∈ V ↦ 𝑅 ) = ( 𝑧 ∈ V ↦ 𝑅 ) )
16 eqidd ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) ∧ 𝑧 = 1 ) → 𝑅 = 𝑅 )
17 1ex ⊢ 1 ∈ V
18 17 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → 1 ∈ V )
19 simpl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → 𝑅 ∈ 𝑉 )
20 15 16 18 19 fvmptd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → ( ( 𝑧 ∈ V ↦ 𝑅 ) ‘ 1 ) = 𝑅 )
21 14 20 seq1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑅 ) ) ‘ 1 ) = 𝑅 )
22 9 13 21 3eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑟 = 𝑅 ∧ 𝑛 = 1 ) ) → if ( 𝑛 = 0 , ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) , ( seq 1 ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑥 ∘ 𝑟 ) ) , ( 𝑧 ∈ V ↦ 𝑟 ) ) ‘ 𝑛 ) ) = 𝑅 )
23 elex ⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V )
24 1nn0 ⊢ 1 ∈ ℕ0
25 24 a1i ⊢ ( 𝑅 ∈ 𝑉 → 1 ∈ ℕ0 )
26 2 22 23 25 23 ovmpod ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 1 ) = 𝑅 )