Step |
Hyp |
Ref |
Expression |
0 |
|
ccofu |
⊢ ∘func |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
vf |
⊢ 𝑓 |
4 |
|
c1st |
⊢ 1st |
5 |
1
|
cv |
⊢ 𝑔 |
6 |
5 4
|
cfv |
⊢ ( 1st ‘ 𝑔 ) |
7 |
3
|
cv |
⊢ 𝑓 |
8 |
7 4
|
cfv |
⊢ ( 1st ‘ 𝑓 ) |
9 |
6 8
|
ccom |
⊢ ( ( 1st ‘ 𝑔 ) ∘ ( 1st ‘ 𝑓 ) ) |
10 |
|
vx |
⊢ 𝑥 |
11 |
|
c2nd |
⊢ 2nd |
12 |
7 11
|
cfv |
⊢ ( 2nd ‘ 𝑓 ) |
13 |
12
|
cdm |
⊢ dom ( 2nd ‘ 𝑓 ) |
14 |
13
|
cdm |
⊢ dom dom ( 2nd ‘ 𝑓 ) |
15 |
|
vy |
⊢ 𝑦 |
16 |
10
|
cv |
⊢ 𝑥 |
17 |
16 8
|
cfv |
⊢ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) |
18 |
5 11
|
cfv |
⊢ ( 2nd ‘ 𝑔 ) |
19 |
15
|
cv |
⊢ 𝑦 |
20 |
19 8
|
cfv |
⊢ ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) |
21 |
17 20 18
|
co |
⊢ ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( 2nd ‘ 𝑔 ) ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) |
22 |
16 19 12
|
co |
⊢ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) |
23 |
21 22
|
ccom |
⊢ ( ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( 2nd ‘ 𝑔 ) ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ) |
24 |
10 15 14 14 23
|
cmpo |
⊢ ( 𝑥 ∈ dom dom ( 2nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2nd ‘ 𝑓 ) ↦ ( ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( 2nd ‘ 𝑔 ) ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ) ) |
25 |
9 24
|
cop |
⊢ 〈 ( ( 1st ‘ 𝑔 ) ∘ ( 1st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2nd ‘ 𝑓 ) ↦ ( ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( 2nd ‘ 𝑔 ) ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ) ) 〉 |
26 |
1 3 2 2 25
|
cmpo |
⊢ ( 𝑔 ∈ V , 𝑓 ∈ V ↦ 〈 ( ( 1st ‘ 𝑔 ) ∘ ( 1st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2nd ‘ 𝑓 ) ↦ ( ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( 2nd ‘ 𝑔 ) ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ) ) 〉 ) |
27 |
0 26
|
wceq |
⊢ ∘func = ( 𝑔 ∈ V , 𝑓 ∈ V ↦ 〈 ( ( 1st ‘ 𝑔 ) ∘ ( 1st ‘ 𝑓 ) ) , ( 𝑥 ∈ dom dom ( 2nd ‘ 𝑓 ) , 𝑦 ∈ dom dom ( 2nd ‘ 𝑓 ) ↦ ( ( ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) ( 2nd ‘ 𝑔 ) ( ( 1st ‘ 𝑓 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2nd ‘ 𝑓 ) 𝑦 ) ) ) 〉 ) |