Detailed syntax breakdown of Definition df-itco
Step | Hyp | Ref
| Expression |
1 | | citco 45421 |
. 2
class
IterComp |
2 | | vf |
. . 3
setvar 𝑓 |
3 | | cvv 3407 |
. . 3
class
V |
4 | | vg |
. . . . 5
setvar 𝑔 |
5 | | vj |
. . . . 5
setvar 𝑗 |
6 | 2 | cv 1538 |
. . . . . 6
class 𝑓 |
7 | 4 | cv 1538 |
. . . . . 6
class 𝑔 |
8 | 6, 7 | ccom 5521 |
. . . . 5
class (𝑓 ∘ 𝑔) |
9 | 4, 5, 3, 3, 8 | cmpo 7145 |
. . . 4
class (𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)) |
10 | | vi |
. . . . 5
setvar 𝑖 |
11 | | cn0 11919 |
. . . . 5
class
ℕ0 |
12 | 10 | cv 1538 |
. . . . . . 7
class 𝑖 |
13 | | cc0 10560 |
. . . . . . 7
class
0 |
14 | 12, 13 | wceq 1539 |
. . . . . 6
wff 𝑖 = 0 |
15 | | cid 5422 |
. . . . . . 7
class
I |
16 | 6 | cdm 5517 |
. . . . . . 7
class dom 𝑓 |
17 | 15, 16 | cres 5519 |
. . . . . 6
class ( I
↾ dom 𝑓) |
18 | 14, 17, 6 | cif 4413 |
. . . . 5
class if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓) |
19 | 10, 11, 18 | cmpt 5105 |
. . . 4
class (𝑖 ∈ ℕ0
↦ if(𝑖 = 0, ( I
↾ dom 𝑓), 𝑓)) |
20 | 9, 19, 13 | cseq 13403 |
. . 3
class
seq0((𝑔 ∈ V,
𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓))) |
21 | 2, 3, 20 | cmpt 5105 |
. 2
class (𝑓 ∈ V ↦ seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)))) |
22 | 1, 21 | wceq 1539 |
1
wff IterComp =
(𝑓 ∈ V ↦
seq0((𝑔 ∈ V, 𝑗 ∈ V ↦ (𝑓 ∘ 𝑔)), (𝑖 ∈ ℕ0 ↦ if(𝑖 = 0, ( I ↾ dom 𝑓), 𝑓)))) |