Metamath Proof Explorer


Theorem itcoval1

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

Ref Expression
Assertion itcoval1 Rel F F V IterComp F 1 = F

Proof

Step Hyp Ref Expression
1 itcoval F V IterComp F = seq 0 g V , j V F g i 0 if i = 0 I dom F F
2 1 fveq1d F V IterComp F 1 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 1
3 2 adantl Rel F F V IterComp F 1 = seq 0 g V , j V F g i 0 if i = 0 I dom F F 1
4 nn0uz 0 = 0
5 0nn0 0 0
6 5 a1i Rel F F V 0 0
7 1e0p1 1 = 0 + 1
8 1 eqcomd F V seq 0 g V , j V F g i 0 if i = 0 I dom F F = IterComp F
9 8 fveq1d F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 0 = IterComp F 0
10 itcoval0 F V IterComp F 0 = I dom F
11 9 10 eqtrd F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 0 = I dom F
12 11 adantl Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 0 = I dom F
13 eqidd Rel F F V i 0 if i = 0 I dom F F = i 0 if i = 0 I dom F F
14 ax-1ne0 1 0
15 14 neii ¬ 1 = 0
16 eqeq1 i = 1 i = 0 1 = 0
17 15 16 mtbiri i = 1 ¬ i = 0
18 17 iffalsed i = 1 if i = 0 I dom F F = F
19 18 adantl Rel F F V i = 1 if i = 0 I dom F F = F
20 1nn0 1 0
21 20 a1i Rel F F V 1 0
22 simpr Rel F F V F V
23 13 19 21 22 fvmptd Rel F F V i 0 if i = 0 I dom F F 1 = F
24 4 6 7 12 23 seqp1d Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 1 = I dom F g V , j V F g F
25 eqidd F V g V , j V F g = g V , j V F g
26 coeq2 g = I dom F F g = F I dom F
27 26 ad2antrl F V g = I dom F j = F F g = F I dom F
28 dmexg F V dom F V
29 28 resiexd F V I dom F V
30 elex F V F V
31 coexg F V I dom F V F I dom F V
32 29 31 mpdan F V F I dom F V
33 25 27 29 30 32 ovmpod F V I dom F g V , j V F g F = F I dom F
34 33 adantl Rel F F V I dom F g V , j V F g F = F I dom F
35 coires1 F I dom F = F dom F
36 resdm Rel F F dom F = F
37 36 adantr Rel F F V F dom F = F
38 35 37 eqtrid Rel F F V F I dom F = F
39 34 38 eqtrd Rel F F V I dom F g V , j V F g F = F
40 24 39 eqtrd Rel F F V seq 0 g V , j V F g i 0 if i = 0 I dom F F 1 = F
41 3 40 eqtrd Rel F F V IterComp F 1 = F