Metamath Proof Explorer


Theorem itcoval1

Description: A function iterated once. (Contributed by AV, 2-May-2024)

Ref Expression
Assertion itcoval1 ( ( Rel 𝐹𝐹𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 itcoval ( 𝐹𝑉 → ( IterComp ‘ 𝐹 ) = seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) )
2 1 fveq1d ( 𝐹𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) )
3 2 adantl ( ( Rel 𝐹𝐹𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) )
4 nn0uz 0 = ( ℤ ‘ 0 )
5 0nn0 0 ∈ ℕ0
6 5 a1i ( ( Rel 𝐹𝐹𝑉 ) → 0 ∈ ℕ0 )
7 1e0p1 1 = ( 0 + 1 )
8 1 eqcomd ( 𝐹𝑉 → seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) = ( IterComp ‘ 𝐹 ) )
9 8 fveq1d ( 𝐹𝑉 → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( ( IterComp ‘ 𝐹 ) ‘ 0 ) )
10 itcoval0 ( 𝐹𝑉 → ( ( IterComp ‘ 𝐹 ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
11 9 10 eqtrd ( 𝐹𝑉 → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
12 11 adantl ( ( Rel 𝐹𝐹𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 0 ) = ( I ↾ dom 𝐹 ) )
13 eqidd ( ( Rel 𝐹𝐹𝑉 ) → ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) )
14 ax-1ne0 1 ≠ 0
15 14 neii ¬ 1 = 0
16 eqeq1 ( 𝑖 = 1 → ( 𝑖 = 0 ↔ 1 = 0 ) )
17 15 16 mtbiri ( 𝑖 = 1 → ¬ 𝑖 = 0 )
18 17 iffalsed ( 𝑖 = 1 → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 )
19 18 adantl ( ( ( Rel 𝐹𝐹𝑉 ) ∧ 𝑖 = 1 ) → if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) = 𝐹 )
20 1nn0 1 ∈ ℕ0
21 20 a1i ( ( Rel 𝐹𝐹𝑉 ) → 1 ∈ ℕ0 )
22 simpr ( ( Rel 𝐹𝐹𝑉 ) → 𝐹𝑉 )
23 13 19 21 22 fvmptd ( ( Rel 𝐹𝐹𝑉 ) → ( ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ‘ 1 ) = 𝐹 )
24 4 6 7 12 23 seqp1d ( ( Rel 𝐹𝐹𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) = ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) 𝐹 ) )
25 eqidd ( 𝐹𝑉 → ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) = ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) )
26 coeq2 ( 𝑔 = ( I ↾ dom 𝐹 ) → ( 𝐹𝑔 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) )
27 26 ad2antrl ( ( 𝐹𝑉 ∧ ( 𝑔 = ( I ↾ dom 𝐹 ) ∧ 𝑗 = 𝐹 ) ) → ( 𝐹𝑔 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) )
28 dmexg ( 𝐹𝑉 → dom 𝐹 ∈ V )
29 28 resiexd ( 𝐹𝑉 → ( I ↾ dom 𝐹 ) ∈ V )
30 elex ( 𝐹𝑉𝐹 ∈ V )
31 coexg ( ( 𝐹𝑉 ∧ ( I ↾ dom 𝐹 ) ∈ V ) → ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ∈ V )
32 29 31 mpdan ( 𝐹𝑉 → ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) ∈ V )
33 25 27 29 30 32 ovmpod ( 𝐹𝑉 → ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) )
34 33 adantl ( ( Rel 𝐹𝐹𝑉 ) → ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) 𝐹 ) = ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) )
35 coires1 ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) = ( 𝐹 ↾ dom 𝐹 )
36 resdm ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
37 36 adantr ( ( Rel 𝐹𝐹𝑉 ) → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
38 35 37 syl5eq ( ( Rel 𝐹𝐹𝑉 ) → ( 𝐹 ∘ ( I ↾ dom 𝐹 ) ) = 𝐹 )
39 34 38 eqtrd ( ( Rel 𝐹𝐹𝑉 ) → ( ( I ↾ dom 𝐹 ) ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) 𝐹 ) = 𝐹 )
40 24 39 eqtrd ( ( Rel 𝐹𝐹𝑉 ) → ( seq 0 ( ( 𝑔 ∈ V , 𝑗 ∈ V ↦ ( 𝐹𝑔 ) ) , ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , ( I ↾ dom 𝐹 ) , 𝐹 ) ) ) ‘ 1 ) = 𝐹 )
41 3 40 eqtrd ( ( Rel 𝐹𝐹𝑉 ) → ( ( IterComp ‘ 𝐹 ) ‘ 1 ) = 𝐹 )