Step | Hyp | Ref
| Expression |
1 | | ccofu 16869 |
. 2
class
∘_{func} |
2 | | vg |
. . 3
setvar 𝑔 |
3 | | vf |
. . 3
setvar 𝑓 |
4 | | cvv 3415 |
. . 3
class
V |
5 | 2 | cv 1657 |
. . . . . 6
class 𝑔 |
6 | | c1st 7427 |
. . . . . 6
class
1^{st} |
7 | 5, 6 | cfv 6124 |
. . . . 5
class
(1^{st} ‘𝑔) |
8 | 3 | cv 1657 |
. . . . . 6
class 𝑓 |
9 | 8, 6 | cfv 6124 |
. . . . 5
class
(1^{st} ‘𝑓) |
10 | 7, 9 | ccom 5347 |
. . . 4
class
((1^{st} ‘𝑔) ∘ (1^{st} ‘𝑓)) |
11 | | vx |
. . . . 5
setvar 𝑥 |
12 | | vy |
. . . . 5
setvar 𝑦 |
13 | | c2nd 7428 |
. . . . . . . 8
class
2^{nd} |
14 | 8, 13 | cfv 6124 |
. . . . . . 7
class
(2^{nd} ‘𝑓) |
15 | 14 | cdm 5343 |
. . . . . 6
class dom
(2^{nd} ‘𝑓) |
16 | 15 | cdm 5343 |
. . . . 5
class dom dom
(2^{nd} ‘𝑓) |
17 | 11 | cv 1657 |
. . . . . . . 8
class 𝑥 |
18 | 17, 9 | cfv 6124 |
. . . . . . 7
class
((1^{st} ‘𝑓)‘𝑥) |
19 | 12 | cv 1657 |
. . . . . . . 8
class 𝑦 |
20 | 19, 9 | cfv 6124 |
. . . . . . 7
class
((1^{st} ‘𝑓)‘𝑦) |
21 | 5, 13 | cfv 6124 |
. . . . . . 7
class
(2^{nd} ‘𝑔) |
22 | 18, 20, 21 | co 6906 |
. . . . . 6
class
(((1^{st} ‘𝑓)‘𝑥)(2^{nd} ‘𝑔)((1^{st} ‘𝑓)‘𝑦)) |
23 | 17, 19, 14 | co 6906 |
. . . . . 6
class (𝑥(2^{nd} ‘𝑓)𝑦) |
24 | 22, 23 | ccom 5347 |
. . . . 5
class
((((1^{st} ‘𝑓)‘𝑥)(2^{nd} ‘𝑔)((1^{st} ‘𝑓)‘𝑦)) ∘ (𝑥(2^{nd} ‘𝑓)𝑦)) |
25 | 11, 12, 16, 16, 24 | cmpt2 6908 |
. . . 4
class (𝑥 ∈ dom dom (2^{nd}
‘𝑓), 𝑦 ∈ dom dom (2^{nd}
‘𝑓) ↦
((((1^{st} ‘𝑓)‘𝑥)(2^{nd} ‘𝑔)((1^{st} ‘𝑓)‘𝑦)) ∘ (𝑥(2^{nd} ‘𝑓)𝑦))) |
26 | 10, 25 | cop 4404 |
. . 3
class
⟨((1^{st} ‘𝑔) ∘ (1^{st} ‘𝑓)), (𝑥 ∈ dom dom (2^{nd} ‘𝑓), 𝑦 ∈ dom dom (2^{nd} ‘𝑓) ↦ ((((1^{st}
‘𝑓)‘𝑥)(2^{nd} ‘𝑔)((1^{st} ‘𝑓)‘𝑦)) ∘ (𝑥(2^{nd} ‘𝑓)𝑦)))⟩ |
27 | 2, 3, 4, 4, 26 | cmpt2 6908 |
. 2
class (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1^{st}
‘𝑔) ∘
(1^{st} ‘𝑓)),
(𝑥 ∈ dom dom
(2^{nd} ‘𝑓),
𝑦 ∈ dom dom
(2^{nd} ‘𝑓)
↦ ((((1^{st} ‘𝑓)‘𝑥)(2^{nd} ‘𝑔)((1^{st} ‘𝑓)‘𝑦)) ∘ (𝑥(2^{nd} ‘𝑓)𝑦)))⟩) |
28 | 1, 27 | wceq 1658 |
1
wff
∘_{func} = (𝑔 ∈ V, 𝑓 ∈ V ↦ ⟨((1^{st}
‘𝑔) ∘
(1^{st} ‘𝑓)),
(𝑥 ∈ dom dom
(2^{nd} ‘𝑓),
𝑦 ∈ dom dom
(2^{nd} ‘𝑓)
↦ ((((1^{st} ‘𝑓)‘𝑥)(2^{nd} ‘𝑔)((1^{st} ‘𝑓)‘𝑦)) ∘ (𝑥(2^{nd} ‘𝑓)𝑦)))⟩) |