Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
2 | | cofucl.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
3 | | cofucl.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) |
4 | 1, 2, 3 | cofuval 17257 |
. . 3
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 〈((1st
‘𝐺) ∘
(1st ‘𝐹)),
(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉) |
5 | 1, 2, 3 | cofu1st 17258 |
. . . 4
⊢ (𝜑 → (1st
‘(𝐺
∘func 𝐹)) = ((1st ‘𝐺) ∘ (1st
‘𝐹))) |
6 | 4 | fveq2d 6678 |
. . . . 5
⊢ (𝜑 → (2nd
‘(𝐺
∘func 𝐹)) = (2nd
‘〈((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉)) |
7 | | fvex 6687 |
. . . . . . 7
⊢
(1st ‘𝐺) ∈ V |
8 | | fvex 6687 |
. . . . . . 7
⊢
(1st ‘𝐹) ∈ V |
9 | 7, 8 | coex 7661 |
. . . . . 6
⊢
((1st ‘𝐺) ∘ (1st ‘𝐹)) ∈ V |
10 | | fvex 6687 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
11 | 10, 10 | mpoex 7803 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) ∈ V |
12 | 9, 11 | op2nd 7723 |
. . . . 5
⊢
(2nd ‘〈((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) |
13 | 6, 12 | eqtrdi 2789 |
. . . 4
⊢ (𝜑 → (2nd
‘(𝐺
∘func 𝐹)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))) |
14 | 5, 13 | opeq12d 4769 |
. . 3
⊢ (𝜑 → 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 =
〈((1st ‘𝐺) ∘ (1st ‘𝐹)), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)))〉) |
15 | 4, 14 | eqtr4d 2776 |
. 2
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉) |
16 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐷) =
(Base‘𝐷) |
17 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝐸) =
(Base‘𝐸) |
18 | | relfunc 17237 |
. . . . . . . 8
⊢ Rel
(𝐷 Func 𝐸) |
19 | | 1st2ndbr 7766 |
. . . . . . . 8
⊢ ((Rel
(𝐷 Func 𝐸) ∧ 𝐺 ∈ (𝐷 Func 𝐸)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺)) |
20 | 18, 3, 19 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺)) |
21 | 16, 17, 20 | funcf1 17241 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐷)⟶(Base‘𝐸)) |
22 | | relfunc 17237 |
. . . . . . . 8
⊢ Rel
(𝐶 Func 𝐷) |
23 | | 1st2ndbr 7766 |
. . . . . . . 8
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
24 | 22, 2, 23 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
25 | 1, 16, 24 | funcf1 17241 |
. . . . . 6
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
26 | | fco 6528 |
. . . . . 6
⊢
(((1st ‘𝐺):(Base‘𝐷)⟶(Base‘𝐸) ∧ (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) → ((1st ‘𝐺) ∘ (1st
‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸)) |
27 | 21, 25, 26 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ((1st
‘𝐺) ∘
(1st ‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸)) |
28 | 5 | feq1d 6489 |
. . . . 5
⊢ (𝜑 → ((1st
‘(𝐺
∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ↔ ((1st ‘𝐺) ∘ (1st
‘𝐹)):(Base‘𝐶)⟶(Base‘𝐸))) |
29 | 27, 28 | mpbird 260 |
. . . 4
⊢ (𝜑 → (1st
‘(𝐺
∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸)) |
30 | | eqid 2738 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) |
31 | | ovex 7203 |
. . . . . . . 8
⊢
(((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∈ V |
32 | | ovex 7203 |
. . . . . . . 8
⊢ (𝑥(2nd ‘𝐹)𝑦) ∈ V |
33 | 31, 32 | coex 7661 |
. . . . . . 7
⊢
((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ V |
34 | 30, 33 | fnmpoi 7793 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶)) |
35 | 13 | fneq1d 6431 |
. . . . . 6
⊢ (𝜑 → ((2nd
‘(𝐺
∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ↔ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) Fn ((Base‘𝐶) × (Base‘𝐶)))) |
36 | 34, 35 | mpbiri 261 |
. . . . 5
⊢ (𝜑 → (2nd
‘(𝐺
∘func 𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶))) |
37 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
38 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
39 | 20 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺)) |
40 | 25 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
41 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
42 | 40, 41 | ffvelrnd 6862 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
43 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
44 | 40, 43 | ffvelrnd 6862 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
45 | 16, 37, 38, 39, 42, 44 | funcf2 17243 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))⟶(((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
46 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
47 | 24 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
48 | 1, 46, 37, 47, 41, 43 | funcf2 17243 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
49 | | fco 6528 |
. . . . . . . . . 10
⊢
(((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))⟶(((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∧ (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
50 | 45, 48, 49 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
51 | | ovex 7203 |
. . . . . . . . . 10
⊢
(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∈ V |
52 | | ovex 7203 |
. . . . . . . . . 10
⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V |
53 | 51, 52 | elmap 8481 |
. . . . . . . . 9
⊢
(((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦)) ↔ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
54 | 50, 53 | sylibr 237 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) ∈ ((((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦))) |
55 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷)) |
56 | 3 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸)) |
57 | 1, 55, 56, 41, 43 | cofu2nd 17260 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) |
58 | 1, 55, 56, 41 | cofu1 17259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑥) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑥))) |
59 | 1, 55, 56, 43 | cofu1 17259 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑦) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))) |
60 | 58, 59 | oveq12d 7188 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) = (((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
61 | 60 | oveq1d 7185 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)) = ((((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ↑m (𝑥(Hom ‘𝐶)𝑦))) |
62 | 54, 57, 61 | 3eltr4d 2848 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))) |
63 | 62 | ralrimivva 3103 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))) |
64 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2nd ‘(𝐺 ∘func
𝐹))‘𝑧) = ((2nd
‘(𝐺
∘func 𝐹))‘〈𝑥, 𝑦〉)) |
65 | | df-ov 7173 |
. . . . . . . . 9
⊢ (𝑥(2nd ‘(𝐺 ∘func
𝐹))𝑦) = ((2nd ‘(𝐺 ∘func
𝐹))‘〈𝑥, 𝑦〉) |
66 | 64, 65 | eqtr4di 2791 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2nd ‘(𝐺 ∘func
𝐹))‘𝑧) = (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)) |
67 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
68 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
69 | 67, 68 | op1std 7724 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
70 | 69 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘(𝐺 ∘func
𝐹))‘(1st
‘𝑧)) =
((1st ‘(𝐺
∘func 𝐹))‘𝑥)) |
71 | 67, 68 | op2ndd 7725 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
72 | 71 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘(𝐺 ∘func
𝐹))‘(2nd
‘𝑧)) =
((1st ‘(𝐺
∘func 𝐹))‘𝑦)) |
73 | 70, 72 | oveq12d 7188 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((1st ‘(𝐺 ∘func
𝐹))‘(1st
‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func
𝐹))‘(2nd
‘𝑧))) =
(((1st ‘(𝐺
∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦))) |
74 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((Hom ‘𝐶)‘𝑧) = ((Hom ‘𝐶)‘〈𝑥, 𝑦〉)) |
75 | | df-ov 7173 |
. . . . . . . . . 10
⊢ (𝑥(Hom ‘𝐶)𝑦) = ((Hom ‘𝐶)‘〈𝑥, 𝑦〉) |
76 | 74, 75 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((Hom ‘𝐶)‘𝑧) = (𝑥(Hom ‘𝐶)𝑦)) |
77 | 73, 76 | oveq12d 7188 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((((1st
‘(𝐺
∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧)) = ((((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))) |
78 | 66, 77 | eleq12d 2827 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((2nd ‘(𝐺 ∘func
𝐹))‘𝑧) ∈ ((((1st
‘(𝐺
∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧)) ↔ (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦)))) |
79 | 78 | ralxp 5684 |
. . . . . 6
⊢
(∀𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func
𝐹))‘(1st
‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func
𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) ∈ ((((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↑m (𝑥(Hom ‘𝐶)𝑦))) |
80 | 63, 79 | sylibr 237 |
. . . . 5
⊢ (𝜑 → ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func 𝐹))‘𝑧) ∈ ((((1st ‘(𝐺 ∘func
𝐹))‘(1st
‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func
𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧))) |
81 | | fvex 6687 |
. . . . . 6
⊢
(2nd ‘(𝐺 ∘func 𝐹)) ∈ V |
82 | 81 | elixp 8514 |
. . . . 5
⊢
((2nd ‘(𝐺 ∘func 𝐹)) ∈ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))((((1st ‘(𝐺 ∘func
𝐹))‘(1st
‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func
𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧)) ↔ ((2nd ‘(𝐺 ∘func
𝐹)) Fn ((Base‘𝐶) × (Base‘𝐶)) ∧ ∀𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((2nd ‘(𝐺 ∘func
𝐹))‘𝑧) ∈ ((((1st
‘(𝐺
∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧)))) |
83 | 36, 80, 82 | sylanbrc 586 |
. . . 4
⊢ (𝜑 → (2nd
‘(𝐺
∘func 𝐹)) ∈ X𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))((((1st
‘(𝐺
∘func 𝐹))‘(1st ‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧))) |
84 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Id‘𝐶) =
(Id‘𝐶) |
85 | | eqid 2738 |
. . . . . . . . . 10
⊢
(Id‘𝐷) =
(Id‘𝐷) |
86 | 24 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
87 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
88 | 1, 84, 85, 86, 87 | funcid 17245 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) |
89 | 88 | fveq2d 6678 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)))) |
90 | | eqid 2738 |
. . . . . . . . 9
⊢
(Id‘𝐸) =
(Id‘𝐸) |
91 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺)) |
92 | 25 | ffvelrnda 6861 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
93 | 16, 85, 90, 91, 92 | funcid 17245 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)))) |
94 | 89, 93 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥))) = ((Id‘𝐸)‘((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)))) |
95 | 2 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷)) |
96 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐷 Func 𝐸)) |
97 | | funcrcl 17238 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
98 | 2, 97 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
99 | 98 | simpld 498 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ Cat) |
100 | 99 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat) |
101 | 1, 46, 84, 100, 87 | catidcl 17056 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) |
102 | 1, 95, 96, 87, 87, 46, 101 | cofu2 17261 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑥))‘((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)))) |
103 | 1, 95, 96, 87 | cofu1 17259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑥) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑥))) |
104 | 103 | fveq2d 6678 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐸)‘((1st ‘(𝐺 ∘func
𝐹))‘𝑥)) = ((Id‘𝐸)‘((1st
‘𝐺)‘((1st ‘𝐹)‘𝑥)))) |
105 | 94, 102, 104 | 3eqtr4d 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func
𝐹))‘𝑥))) |
106 | 86 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
107 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑥 ∈ (Base‘𝐶)) |
108 | | simprlr 780 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑧 ∈ (Base‘𝐶)) |
109 | 1, 46, 37, 106, 107, 108 | funcf2 17243 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
110 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(comp‘𝐶) =
(comp‘𝐶) |
111 | 100 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐶 ∈ Cat) |
112 | | simprll 779 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑦 ∈ (Base‘𝐶)) |
113 | | simprrl 781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
114 | | simprrr 782 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
115 | 1, 46, 110, 111, 107, 112, 108, 113, 114 | catcocl 17059 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
116 | | fvco3 6767 |
. . . . . . . . . . . 12
⊢ (((𝑥(2nd ‘𝐹)𝑧):(𝑥(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧)) ∧ (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
117 | 109, 115,
116 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)))) |
118 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(comp‘𝐷) =
(comp‘𝐷) |
119 | 1, 46, 110, 118, 106, 107, 112, 108, 113, 114 | funcco 17246 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))) |
120 | 119 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))) |
121 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(comp‘𝐸) =
(comp‘𝐸) |
122 | 91 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐺)(𝐷 Func 𝐸)(2nd ‘𝐺)) |
123 | 92 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
124 | 25 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
125 | 124 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
126 | 125, 112 | ffvelrnd 6862 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
127 | 125, 108 | ffvelrnd 6862 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷)) |
128 | 1, 46, 37, 106, 107, 112 | funcf2 17243 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
129 | 128, 113 | ffvelrnd 6862 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
130 | 1, 46, 37, 106, 112, 108 | funcf2 17243 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
131 | 130, 114 | ffvelrnd 6862 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
132 | 16, 37, 118, 121, 122, 123, 126, 127, 129, 131 | funcco 17246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))) = (((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))(〈((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)), ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))〉(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))) |
133 | 117, 120,
132 | 3eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))(〈((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)), ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))〉(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))) |
134 | 95 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐹 ∈ (𝐶 Func 𝐷)) |
135 | 96 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 𝐺 ∈ (𝐷 Func 𝐸)) |
136 | 1, 134, 135, 107, 108 | cofu2nd 17260 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))) |
137 | 136 | fveq1d 6676 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧)) ∘ (𝑥(2nd ‘𝐹)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))) |
138 | 103 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑥) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑥))) |
139 | 1, 134, 135, 112 | cofu1 17259 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑦) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))) |
140 | 138, 139 | opeq12d 4769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → 〈((1st
‘(𝐺
∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)〉 = 〈((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)), ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))〉) |
141 | 1, 134, 135, 108 | cofu1 17259 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑧) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑧))) |
142 | 140, 141 | oveq12d 7188 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (〈((1st
‘(𝐺
∘func 𝐹))‘𝑥), ((1st ‘(𝐺 ∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧)) = (〈((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)), ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))〉(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))) |
143 | 1, 134, 135, 112, 108, 46, 114 | cofu2 17261 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔) = ((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))) |
144 | 1, 134, 135, 107, 112, 46, 113 | cofu2 17261 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓))) |
145 | 142, 143,
144 | oveq123d 7191 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)) = (((((1st ‘𝐹)‘𝑦)(2nd ‘𝐺)((1st ‘𝐹)‘𝑧))‘((𝑦(2nd ‘𝐹)𝑧)‘𝑔))(〈((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥)), ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))〉(comp‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑧)))((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦))‘((𝑥(2nd ‘𝐹)𝑦)‘𝑓)))) |
146 | 133, 137,
145 | 3eqtr4d 2783 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ ((𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))) |
147 | 146 | anassrs 471 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))) |
148 | 147 | ralrimivva 3103 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶))) → ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))) |
149 | 148 | ralrimivva 3103 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓))) |
150 | 105, 149 | jca 515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func
𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))) |
151 | 150 | ralrimiva 3096 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)(((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func
𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))) |
152 | | funcrcl 17238 |
. . . . . . 7
⊢ (𝐺 ∈ (𝐷 Func 𝐸) → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
153 | 3, 152 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐷 ∈ Cat ∧ 𝐸 ∈ Cat)) |
154 | 153 | simprd 499 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ Cat) |
155 | 1, 17, 46, 38, 84, 90, 110, 121, 99, 154 | isfunc 17239 |
. . . 4
⊢ (𝜑 → ((1st
‘(𝐺
∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ((1st
‘(𝐺
∘func 𝐹)):(Base‘𝐶)⟶(Base‘𝐸) ∧ (2nd ‘(𝐺 ∘func
𝐹)) ∈ X𝑧 ∈
((Base‘𝐶) ×
(Base‘𝐶))((((1st ‘(𝐺 ∘func
𝐹))‘(1st
‘𝑧))(Hom ‘𝐸)((1st ‘(𝐺 ∘func
𝐹))‘(2nd
‘𝑧)))
↑m ((Hom ‘𝐶)‘𝑧)) ∧ ∀𝑥 ∈ (Base‘𝐶)(((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘(𝐺 ∘func
𝐹))‘𝑥)) ∧ ∀𝑦 ∈ (Base‘𝐶)∀𝑧 ∈ (Base‘𝐶)∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)∀𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘(𝐺 ∘func 𝐹))𝑧)‘𝑔)(〈((1st ‘(𝐺 ∘func
𝐹))‘𝑥), ((1st
‘(𝐺
∘func 𝐹))‘𝑦)〉(comp‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑧))((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦)‘𝑓)))))) |
156 | 29, 83, 151, 155 | mpbir3and 1343 |
. . 3
⊢ (𝜑 → (1st
‘(𝐺
∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹))) |
157 | | df-br 5031 |
. . 3
⊢
((1st ‘(𝐺 ∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 ∈ (𝐶 Func 𝐸)) |
158 | 156, 157 | sylib 221 |
. 2
⊢ (𝜑 → 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 ∈ (𝐶 Func 𝐸)) |
159 | 15, 158 | eqeltrd 2833 |
1
⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) |