Step | Hyp | Ref
| Expression |
1 | | hofcl.m |
. . . 4
⊢ 𝑀 =
(Hom_{F}‘𝐶) |
2 | | hofcl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | eqid 2765 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
4 | | eqid 2765 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | | eqid 2765 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
6 | 1, 2, 3, 4, 5 | hofval 17158 |
. . 3
⊢ (𝜑 → 𝑀 = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))⟩) |
7 | | fvex 6388 |
. . . . . 6
⊢
(Hom_{f} ‘𝐶) ∈ V |
8 | | fvex 6388 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
9 | 8, 8 | xpex 7160 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V |
10 | 9, 9 | mpt2ex 7448 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) ∈ V |
11 | 7, 10 | op2ndd 7377 |
. . . . 5
⊢ (𝑀 = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))⟩ → (2^{nd}
‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))) |
12 | 6, 11 | syl 17 |
. . . 4
⊢ (𝜑 → (2^{nd}
‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))) |
13 | 12 | opeq2d 4566 |
. . 3
⊢ (𝜑 →
⟨(Hom_{f} ‘𝐶), (2^{nd} ‘𝑀)⟩ = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))⟩) |
14 | 6, 13 | eqtr4d 2802 |
. 2
⊢ (𝜑 → 𝑀 = ⟨(Hom_{f}
‘𝐶), (2^{nd}
‘𝑀)⟩) |
15 | | eqid 2765 |
. . . . 5
⊢ (𝑂 ×_{c}
𝐶) = (𝑂 ×_{c} 𝐶) |
16 | | hofcl.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
17 | 16, 3 | oppcbas 16643 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝑂) |
18 | 15, 17, 3 | xpcbas 17084 |
. . . 4
⊢
((Base‘𝐶)
× (Base‘𝐶)) =
(Base‘(𝑂
×_{c} 𝐶)) |
19 | | eqid 2765 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
20 | | eqid 2765 |
. . . 4
⊢ (Hom
‘(𝑂
×_{c} 𝐶)) = (Hom ‘(𝑂 ×_{c} 𝐶)) |
21 | | eqid 2765 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
22 | | eqid 2765 |
. . . 4
⊢
(Id‘(𝑂
×_{c} 𝐶)) = (Id‘(𝑂 ×_{c} 𝐶)) |
23 | | eqid 2765 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
24 | | eqid 2765 |
. . . 4
⊢
(comp‘(𝑂
×_{c} 𝐶)) = (comp‘(𝑂 ×_{c} 𝐶)) |
25 | | eqid 2765 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
26 | 16 | oppccat 16647 |
. . . . . 6
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
27 | 2, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑂 ∈ Cat) |
28 | 15, 27, 2 | xpccat 17096 |
. . . 4
⊢ (𝜑 → (𝑂 ×_{c} 𝐶) ∈ Cat) |
29 | | hofcl.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
30 | | hofcl.d |
. . . . . 6
⊢ 𝐷 = (SetCat‘𝑈) |
31 | 30 | setccat 17000 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → 𝐷 ∈ Cat) |
32 | 29, 31 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
33 | | eqid 2765 |
. . . . . . . 8
⊢
(Hom_{f} ‘𝐶) = (Hom_{f} ‘𝐶) |
34 | 33, 3 | homffn 16618 |
. . . . . . 7
⊢
(Hom_{f} ‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (Hom_{f}
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
36 | | hofcl.h |
. . . . . 6
⊢ (𝜑 → ran
(Hom_{f} ‘𝐶) ⊆ 𝑈) |
37 | | df-f 6072 |
. . . . . 6
⊢
((Hom_{f} ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ ((Hom_{f}
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ∧ ran
(Hom_{f} ‘𝐶) ⊆ 𝑈)) |
38 | 35, 36, 37 | sylanbrc 578 |
. . . . 5
⊢ (𝜑 → (Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) |
39 | 30, 29 | setcbas 16993 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (Base‘𝐷)) |
40 | 39 | feq3d 6210 |
. . . . 5
⊢ (𝜑 → ((Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ (Hom_{f} ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷))) |
41 | 38, 40 | mpbid 223 |
. . . 4
⊢ (𝜑 → (Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷)) |
42 | | eqid 2765 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) |
43 | | ovex 6874 |
. . . . . . 7
⊢
((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∈ V |
44 | | ovex 6874 |
. . . . . . 7
⊢
((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ∈ V |
45 | 43, 44 | mpt2ex 7448 |
. . . . . 6
⊢ (𝑓 ∈ ((1^{st}
‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))) ∈ V |
46 | 42, 45 | fnmpt2i 7440 |
. . . . 5
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))) |
47 | 12 | fneq1d 6159 |
. . . . 5
⊢ (𝜑 → ((2^{nd}
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶))) ↔
(𝑥 ∈
((Base‘𝐶) ×
(Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))))) |
48 | 46, 47 | mpbiri 249 |
. . . 4
⊢ (𝜑 → (2^{nd}
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶)))) |
49 | 2 | ad3antrrr 721 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat) |
50 | | simplrr 796 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
51 | | xp1st 7398 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1^{st}
‘𝑦) ∈
(Base‘𝐶)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
53 | 52 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
54 | | simplrl 795 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
55 | | xp1st 7398 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1^{st}
‘𝑥) ∈
(Base‘𝐶)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
57 | 56 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
58 | | xp2nd 7399 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2^{nd}
‘𝑦) ∈
(Base‘𝐶)) |
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
60 | 59 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
61 | | simplrl 795 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
62 | | 1st2nd2 7405 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
63 | 54, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
64 | 63 | adantr 472 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
65 | 64 | oveq1d 6857 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2^{nd} ‘𝑦)) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))) |
66 | 65 | oveqd 6859 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) = (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)) |
67 | | xp2nd 7399 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2^{nd}
‘𝑥) ∈
(Base‘𝐶)) |
68 | 54, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
69 | 68 | adantr 472 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
70 | 63 | fveq2d 6379 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
71 | | df-ov 6845 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
72 | 70, 71 | syl6eqr 2817 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
73 | 72 | eleq2d 2830 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)))) |
74 | 73 | biimpa 468 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
75 | | simplrr 796 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
76 | 3, 4, 5, 49, 57, 69, 60, 74, 75 | catcocl 16611 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
77 | 66, 76 | eqeltrd 2844 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
78 | 3, 4, 5, 49, 53, 57, 60, 61, 77 | catcocl 16611 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓) ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
79 | | 1st2nd2 7405 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑦 = ⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
80 | 50, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑦 = ⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
81 | 80 | fveq2d 6379 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
82 | | df-ov 6845 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦)) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
83 | 81, 82 | syl6eqr 2817 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
84 | 83 | adantr 472 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((Hom ‘𝐶)‘𝑦) = ((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
85 | 78, 84 | eleqtrrd 2847 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓) ∈ ((Hom ‘𝐶)‘𝑦)) |
86 | 85 | fmpttd 6575 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦)) |
87 | 29 | ad2antrr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑈 ∈ 𝑉) |
88 | 33, 3, 4, 56, 68 | homfval 16617 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((1^{st} ‘𝑥)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑥)) =
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
89 | 63 | fveq2d 6379 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
90 | | df-ov 6845 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥)) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
91 | 89, 90 | syl6eqr 2817 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥))) |
92 | 88, 91, 72 | 3eqtr4d 2809 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘𝑥)) |
93 | 38 | ad2antrr 717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) |
94 | 93, 54 | ffvelrnd 6550 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) ∈ 𝑈) |
95 | 92, 94 | eqeltrrd 2845 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) ∈ 𝑈) |
96 | 33, 3, 4, 52, 59 | homfval 16617 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((1^{st} ‘𝑦)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑦)) =
((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
97 | 80 | fveq2d 6379 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
98 | | df-ov 6845 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑦)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑦)) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
99 | 97, 98 | syl6eqr 2817 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((1^{st}
‘𝑦)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑦))) |
100 | 96, 99, 83 | 3eqtr4d 2809 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘𝑦)) |
101 | 93, 50 | ffvelrnd 6550 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) ∈ 𝑈) |
102 | 100, 101 | eqeltrrd 2845 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) ∈ 𝑈) |
103 | 30, 87, 21, 95, 102 | elsetchom 16996 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)) ↔ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦))) |
104 | 86, 103 | mpbird 248 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) |
105 | 92, 100 | oveq12d 6860 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦)) = (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) |
106 | 104, 105 | eleqtrrd 2847 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) ∈ (((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦))) |
107 | 106 | ralrimivva 3118 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ∀𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))∀𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) ∈ (((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦))) |
108 | | eqid 2765 |
. . . . . . 7
⊢ (𝑓 ∈ ((1^{st}
‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))) = (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))) |
109 | 108 | fmpt2 7438 |
. . . . . 6
⊢
(∀𝑓 ∈
((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))∀𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) ∈ (((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))):(((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))⟶(((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦))) |
110 | 107, 109 | sylib 209 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))):(((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))⟶(((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦))) |
111 | 12 | oveqd 6859 |
. . . . . . 7
⊢ (𝜑 → (𝑥(2^{nd} ‘𝑀)𝑦) = (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))𝑦)) |
112 | 42 | ovmpt4g 6981 |
. . . . . . . 8
⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))) ∈ V) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) |
113 | 45, 112 | mp3an3 1574 |
. . . . . . 7
⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) |
114 | 111, 113 | sylan9eq 2819 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2^{nd} ‘𝑀)𝑦) = (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) |
115 | | eqid 2765 |
. . . . . . . 8
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
116 | | simprl 787 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
117 | | simprr 789 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
118 | 15, 18, 115, 4, 20, 116, 117 | xpchom 17086 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) = (((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
119 | 4, 16 | oppchom 16640 |
. . . . . . . 8
⊢
((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) = ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) |
120 | 119 | xpeq1i 5303 |
. . . . . . 7
⊢
(((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) = (((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
121 | 118, 120 | syl6eq 2815 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) = (((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
122 | 114, 121 | feq12d 6211 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((𝑥(2^{nd} ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦)⟶(((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))):(((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))⟶(((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦)))) |
123 | 110, 122 | mpbird 248 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2^{nd} ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦)⟶(((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦))) |
124 | | eqid 2765 |
. . . . . . . . . 10
⊢
(Id‘𝐶) =
(Id‘𝐶) |
125 | 2 | ad2antrr 717 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → 𝐶 ∈ Cat) |
126 | 55 | adantl 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
127 | 126 | adantr 472 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
128 | 67 | adantl 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
129 | 128 | adantr 472 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
130 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
131 | 3, 4, 124, 125, 127, 5, 129, 130 | catlid 16609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓) = 𝑓) |
132 | 131 | oveq1d 6857 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → ((((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥))) = (𝑓(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥)))) |
133 | 3, 4, 124, 125, 127, 5, 129, 130 | catrid 16610 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (𝑓(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥))) = 𝑓) |
134 | 132, 133 | eqtrd 2799 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → ((((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥))) = 𝑓) |
135 | 134 | mpteq2dva 4903 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ ((((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥)))) = (𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ 𝑓)) |
136 | | df-ov 6845 |
. . . . . . 7
⊢
(((Id‘𝐶)‘(1^{st} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)((Id‘𝐶)‘(2^{nd} ‘𝑥))) = ((⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
137 | 2 | adantr 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝐶 ∈ Cat) |
138 | 3, 4, 124, 137, 126 | catidcl 16608 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(1^{st} ‘𝑥)) ∈ ((1^{st}
‘𝑥)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
139 | 3, 4, 124, 137, 128 | catidcl 16608 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(2^{nd} ‘𝑥)) ∈ ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
140 | 1, 137, 3, 4, 126, 128, 126, 128, 5, 138, 139 | hof2val 17162 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((Id‘𝐶)‘(1^{st} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)((Id‘𝐶)‘(2^{nd} ‘𝑥))) = (𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ ((((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥))))) |
141 | 136, 140 | syl5eqr 2813 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) = (𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ ((((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥))))) |
142 | 62 | adantl 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
143 | 142 | fveq2d 6379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
144 | 143, 90 | syl6eqr 2817 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥))) |
145 | 33, 3, 4, 126, 128 | homfval 16617 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((1^{st} ‘𝑥)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑥)) =
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
146 | 144, 145 | eqtrd 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
147 | 146 | reseq2d 5565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Hom_{f} ‘𝐶)‘𝑥)) = ( I ↾ ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)))) |
148 | | mptresid 5640 |
. . . . . . 7
⊢ (𝑓 ∈ ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ 𝑓) = ( I ↾ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
149 | 147, 148 | syl6eqr 2817 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Hom_{f} ‘𝐶)‘𝑥)) = (𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ 𝑓)) |
150 | 135, 141,
149 | 3eqtr4d 2809 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) = ( I ↾
((Hom_{f} ‘𝐶)‘𝑥))) |
151 | 142, 142 | oveq12d 6860 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(2^{nd} ‘𝑀)𝑥) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
152 | 142 | fveq2d 6379 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×_{c} 𝐶))‘𝑥) = ((Id‘(𝑂 ×_{c} 𝐶))‘⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)) |
153 | 27 | adantr 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑂 ∈ Cat) |
154 | | eqid 2765 |
. . . . . . . 8
⊢
(Id‘𝑂) =
(Id‘𝑂) |
155 | 15, 153, 137, 17, 3, 154, 124, 22, 126, 128 | xpcid 17095 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×_{c} 𝐶))‘⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩) =
⟨((Id‘𝑂)‘(1^{st} ‘𝑥)), ((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
156 | 16, 124 | oppcid 16646 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) |
157 | 137, 156 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (Id‘𝑂) = (Id‘𝐶)) |
158 | 157 | fveq1d 6377 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝑂)‘(1^{st} ‘𝑥)) = ((Id‘𝐶)‘(1^{st}
‘𝑥))) |
159 | 158 | opeq1d 4565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ⟨((Id‘𝑂)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩ =
⟨((Id‘𝐶)‘(1^{st} ‘𝑥)), ((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
160 | 152, 155,
159 | 3eqtrd 2803 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×_{c} 𝐶))‘𝑥) = ⟨((Id‘𝐶)‘(1^{st} ‘𝑥)), ((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
161 | 151, 160 | fveq12d 6382 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2^{nd} ‘𝑀)𝑥)‘((Id‘(𝑂 ×_{c} 𝐶))‘𝑥)) = ((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩)) |
162 | 29 | adantr 472 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑈 ∈ 𝑉) |
163 | 38 | ffvelrnda 6549 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) ∈ 𝑈) |
164 | 30, 23, 162, 163 | setcid 17001 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐷)‘((Hom_{f}
‘𝐶)‘𝑥)) = ( I ↾
((Hom_{f} ‘𝐶)‘𝑥))) |
165 | 150, 161,
164 | 3eqtr4d 2809 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2^{nd} ‘𝑀)𝑥)‘((Id‘(𝑂 ×_{c} 𝐶))‘𝑥)) = ((Id‘𝐷)‘((Hom_{f}
‘𝐶)‘𝑥))) |
166 | 2 | 3ad2ant1 1163 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝐶 ∈ Cat) |
167 | 29 | 3ad2ant1 1163 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑈 ∈ 𝑉) |
168 | 36 | 3ad2ant1 1163 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ran (Hom_{f}
‘𝐶) ⊆ 𝑈) |
169 | | simp21 1263 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
170 | 169, 55 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
171 | 169, 67 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
172 | | simp22 1264 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
173 | 172, 51 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
174 | 172, 58 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
175 | | simp23 1265 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
176 | | xp1st 7398 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1^{st}
‘𝑧) ∈
(Base‘𝐶)) |
177 | 175, 176 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑧) ∈ (Base‘𝐶)) |
178 | | xp2nd 7399 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2^{nd}
‘𝑧) ∈
(Base‘𝐶)) |
179 | 175, 178 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑧) ∈ (Base‘𝐶)) |
180 | | simp3l 1258 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦)) |
181 | 15, 18, 115, 4, 20, 169, 172 | xpchom 17086 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) = (((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
182 | 180, 181 | eleqtrd 2846 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑓 ∈ (((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
183 | | xp1st 7398 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) → (1^{st}
‘𝑓) ∈
((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦))) |
184 | 182, 183 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑓) ∈ ((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦))) |
185 | 184, 119 | syl6eleq 2854 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑓) ∈ ((1^{st}
‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
186 | | xp2nd 7399 |
. . . . . . 7
⊢ (𝑓 ∈ (((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) → (2^{nd}
‘𝑓) ∈
((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
187 | 182, 186 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑓) ∈ ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
188 | | simp3r 1259 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧)) |
189 | 15, 18, 115, 4, 20, 172, 175 | xpchom 17086 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧) = (((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧)))) |
190 | 188, 189 | eleqtrd 2846 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑔 ∈ (((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧)))) |
191 | | xp1st 7398 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) → (1^{st}
‘𝑔) ∈
((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧))) |
192 | 190, 191 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧))) |
193 | 4, 16 | oppchom 16640 |
. . . . . . 7
⊢
((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) = ((1^{st} ‘𝑧)(Hom ‘𝐶)(1^{st} ‘𝑦)) |
194 | 192, 193 | syl6eleq 2854 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘𝑧)(Hom ‘𝐶)(1^{st} ‘𝑦))) |
195 | | xp2nd 7399 |
. . . . . . 7
⊢ (𝑔 ∈ (((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) → (2^{nd}
‘𝑔) ∈
((2^{nd} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
196 | 190, 195 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑔) ∈ ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
197 | 1, 16, 30, 166, 167, 168, 3, 4, 170, 171, 173, 174, 177, 179, 185, 187, 194, 196 | hofcllem 17164 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (((1^{st} ‘𝑓)(⟨(1^{st}
‘𝑧), (1^{st}
‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔))(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))) = (((1^{st}
‘𝑔)(⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)(2^{nd}
‘𝑔))(⟨((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)), ((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))⟩(comp‘𝐷)((1^{st} ‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧)))((1^{st} ‘𝑓)(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)(2^{nd}
‘𝑓)))) |
198 | 169, 62 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
199 | | 1st2nd2 7405 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩) |
200 | 175, 199 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑧 = ⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩) |
201 | 198, 200 | oveq12d 6860 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑥(2^{nd} ‘𝑀)𝑧) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)) |
202 | 172, 79 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑦 = ⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
203 | 198, 202 | opeq12d 4567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩,
⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩⟩) |
204 | 203, 200 | oveq12d 6860 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (⟨𝑥, 𝑦⟩(comp‘(𝑂 ×_{c} 𝐶))𝑧) = (⟨⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩, ⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩⟩(comp‘(𝑂 ×_{c} 𝐶))⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)) |
205 | | 1st2nd2 7405 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) → 𝑔 = ⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩) |
206 | 190, 205 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑔 = ⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩) |
207 | | 1st2nd2 7405 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) → 𝑓 = ⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) |
208 | 182, 207 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑓 = ⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) |
209 | 204, 206,
208 | oveq123d 6863 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×_{c} 𝐶))𝑧)𝑓) = (⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩(⟨⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩,
⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩⟩(comp‘(𝑂 ×_{c} 𝐶))⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩)) |
210 | | eqid 2765 |
. . . . . . . . 9
⊢
(comp‘𝑂) =
(comp‘𝑂) |
211 | 15, 17, 3, 115, 4, 170, 171, 173, 174, 210, 5, 24, 177, 179, 184, 187, 192, 196 | xpcco2 17093 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (⟨(1^{st}
‘𝑔), (2^{nd}
‘𝑔)⟩(⟨⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩,
⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩⟩(comp‘(𝑂 ×_{c} 𝐶))⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) =
⟨((1^{st} ‘𝑔)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑦)⟩(comp‘𝑂)(1^{st} ‘𝑧))(1^{st} ‘𝑓)), ((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))⟩) |
212 | 3, 5, 16, 170, 173, 177 | oppcco 16642 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑥), (1^{st}
‘𝑦)⟩(comp‘𝑂)(1^{st} ‘𝑧))(1^{st} ‘𝑓)) = ((1^{st} ‘𝑓)(⟨(1^{st}
‘𝑧), (1^{st}
‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔))) |
213 | 212 | opeq1d 4565 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ⟨((1^{st}
‘𝑔)(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑦)⟩(comp‘𝑂)(1^{st} ‘𝑧))(1^{st} ‘𝑓)), ((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))⟩ =
⟨((1^{st} ‘𝑓)(⟨(1^{st} ‘𝑧), (1^{st} ‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔)), ((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))⟩) |
214 | 209, 211,
213 | 3eqtrd 2803 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×_{c} 𝐶))𝑧)𝑓) = ⟨((1^{st} ‘𝑓)(⟨(1^{st}
‘𝑧), (1^{st}
‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔)), ((2^{nd} ‘𝑔)(⟨(2^{nd}
‘𝑥), (2^{nd}
‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))⟩) |
215 | 201, 214 | fveq12d 6382 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑥(2^{nd} ‘𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×_{c} 𝐶))𝑧)𝑓)) = ((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)‘⟨((1^{st}
‘𝑓)(⟨(1^{st} ‘𝑧), (1^{st} ‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔)), ((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))⟩)) |
216 | | df-ov 6845 |
. . . . . 6
⊢
(((1^{st} ‘𝑓)(⟨(1^{st} ‘𝑧), (1^{st} ‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)((2^{nd} ‘𝑔)(⟨(2^{nd}
‘𝑥), (2^{nd}
‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))) = ((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)‘⟨((1^{st}
‘𝑓)(⟨(1^{st} ‘𝑧), (1^{st} ‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔)), ((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓))⟩) |
217 | 215, 216 | syl6eqr 2817 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑥(2^{nd} ‘𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×_{c} 𝐶))𝑧)𝑓)) = (((1^{st} ‘𝑓)(⟨(1^{st}
‘𝑧), (1^{st}
‘𝑦)⟩(comp‘𝐶)(1^{st} ‘𝑥))(1^{st} ‘𝑔))(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)((2^{nd}
‘𝑔)(⟨(2^{nd} ‘𝑥), (2^{nd} ‘𝑦)⟩(comp‘𝐶)(2^{nd} ‘𝑧))(2^{nd} ‘𝑓)))) |
218 | 198 | fveq2d 6379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
219 | 218, 90 | syl6eqr 2817 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥))) |
220 | 33, 3, 4, 170, 171 | homfval 16617 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑥)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑥)) =
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
221 | 219, 220 | eqtrd 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
222 | 202 | fveq2d 6379 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
223 | 222, 98 | syl6eqr 2817 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((1^{st}
‘𝑦)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑦))) |
224 | 33, 3, 4, 173, 174 | homfval 16617 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑦)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑦)) =
((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
225 | 223, 224 | eqtrd 2799 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((1^{st}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
226 | 221, 225 | opeq12d 4567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ⟨((Hom_{f}
‘𝐶)‘𝑥), ((Hom_{f}
‘𝐶)‘𝑦)⟩ = ⟨((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)), ((1^{st}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))⟩) |
227 | 200 | fveq2d 6379 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑧) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)) |
228 | | df-ov 6845 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑧)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑧)) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩) |
229 | 227, 228 | syl6eqr 2817 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑧) = ((1^{st}
‘𝑧)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑧))) |
230 | 33, 3, 4, 177, 179 | homfval 16617 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑧)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑧)) =
((1^{st} ‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
231 | 229, 230 | eqtrd 2799 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑧) = ((1^{st}
‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
232 | 226, 231 | oveq12d 6860 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (⟨((Hom_{f}
‘𝐶)‘𝑥), ((Hom_{f}
‘𝐶)‘𝑦)⟩(comp‘𝐷)((Hom_{f}
‘𝐶)‘𝑧)) = (⟨((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)), ((1^{st}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))⟩(comp‘𝐷)((1^{st} ‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧)))) |
233 | 202, 200 | oveq12d 6860 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑦(2^{nd} ‘𝑀)𝑧) = (⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)) |
234 | 233, 206 | fveq12d 6382 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑦(2^{nd} ‘𝑀)𝑧)‘𝑔) = ((⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)‘⟨(1^{st}
‘𝑔), (2^{nd}
‘𝑔)⟩)) |
235 | | df-ov 6845 |
. . . . . . 7
⊢
((1^{st} ‘𝑔)(⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)(2^{nd}
‘𝑔)) =
((⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)‘⟨(1^{st}
‘𝑔), (2^{nd}
‘𝑔)⟩) |
236 | 234, 235 | syl6eqr 2817 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑦(2^{nd} ‘𝑀)𝑧)‘𝑔) = ((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)(2^{nd} ‘𝑔))) |
237 | 198, 202 | oveq12d 6860 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑥(2^{nd} ‘𝑀)𝑦) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
238 | 237, 208 | fveq12d 6382 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑥(2^{nd} ‘𝑀)𝑦)‘𝑓) = ((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)‘⟨(1^{st}
‘𝑓), (2^{nd}
‘𝑓)⟩)) |
239 | | df-ov 6845 |
. . . . . . 7
⊢
((1^{st} ‘𝑓)(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)(2^{nd}
‘𝑓)) =
((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩)‘⟨(1^{st}
‘𝑓), (2^{nd}
‘𝑓)⟩) |
240 | 238, 239 | syl6eqr 2817 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑥(2^{nd} ‘𝑀)𝑦)‘𝑓) = ((1^{st} ‘𝑓)(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩)(2^{nd} ‘𝑓))) |
241 | 232, 236,
240 | oveq123d 6863 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (((𝑦(2^{nd} ‘𝑀)𝑧)‘𝑔)(⟨((Hom_{f} ‘𝐶)‘𝑥), ((Hom_{f} ‘𝐶)‘𝑦)⟩(comp‘𝐷)((Hom_{f} ‘𝐶)‘𝑧))((𝑥(2^{nd} ‘𝑀)𝑦)‘𝑓)) = (((1^{st} ‘𝑔)(⟨(1^{st}
‘𝑦), (2^{nd}
‘𝑦)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑧), (2^{nd}
‘𝑧)⟩)(2^{nd} ‘𝑔))(⟨((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)), ((1^{st}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))⟩(comp‘𝐷)((1^{st} ‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧)))((1^{st} ‘𝑓)(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)(2^{nd}
‘𝑓)))) |
242 | 197, 217,
241 | 3eqtr4d 2809 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((𝑥(2^{nd} ‘𝑀)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘(𝑂 ×_{c} 𝐶))𝑧)𝑓)) = (((𝑦(2^{nd} ‘𝑀)𝑧)‘𝑔)(⟨((Hom_{f} ‘𝐶)‘𝑥), ((Hom_{f} ‘𝐶)‘𝑦)⟩(comp‘𝐷)((Hom_{f} ‘𝐶)‘𝑧))((𝑥(2^{nd} ‘𝑀)𝑦)‘𝑓))) |
243 | 18, 19, 20, 21, 22, 23, 24, 25, 28, 32, 41, 48, 123, 165, 242 | isfuncd 16790 |
. . 3
⊢ (𝜑 → (Hom_{f}
‘𝐶)((𝑂 ×_{c}
𝐶) Func 𝐷)(2^{nd} ‘𝑀)) |
244 | | df-br 4810 |
. . 3
⊢
((Hom_{f} ‘𝐶)((𝑂 ×_{c} 𝐶) Func 𝐷)(2^{nd} ‘𝑀) ↔ ⟨(Hom_{f}
‘𝐶), (2^{nd}
‘𝑀)⟩ ∈
((𝑂
×_{c} 𝐶) Func 𝐷)) |
245 | 243, 244 | sylib 209 |
. 2
⊢ (𝜑 →
⟨(Hom_{f} ‘𝐶), (2^{nd} ‘𝑀)⟩ ∈ ((𝑂 ×_{c} 𝐶) Func 𝐷)) |
246 | 14, 245 | eqeltrd 2844 |
1
⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×_{c} 𝐶) Func 𝐷)) |