Step | Hyp | Ref
| Expression |
1 | | hofcl.m |
. . . 4
⊢ 𝑀 =
(Hom_{F}‘𝐶) |
2 | | hofcl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
4 | | eqid 2610 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | | eqid 2610 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
6 | 1, 2, 3, 4, 5 | hofval 16715 |
. . 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 6113 |
. . . . . 6
⊢
(Hom_{f} ‘𝐶) ∈ V |
8 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
9 | 8, 8 | xpex 6860 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V |
10 | 9, 9 | mpt2ex 7136 |
. . . . . 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 7070 |
. . . . 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 4347 |
. . 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 2647 |
. 2
⊢ (𝜑 → 𝑀 = ⟨(Hom_{f}
‘𝐶), (2^{nd}
‘𝑀)⟩) |
15 | | eqid 2610 |
. . . . 5
⊢ (𝑂 ×_{c}
𝐶) = (𝑂 ×_{c} 𝐶) |
16 | | hofcl.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
17 | 16, 3 | oppcbas 16201 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝑂) |
18 | 15, 17, 3 | xpcbas 16641 |
. . . 4
⊢
((Base‘𝐶)
× (Base‘𝐶)) =
(Base‘(𝑂
×_{c} 𝐶)) |
19 | | eqid 2610 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
20 | | eqid 2610 |
. . . 4
⊢ (Hom
‘(𝑂
×_{c} 𝐶)) = (Hom ‘(𝑂 ×_{c} 𝐶)) |
21 | | eqid 2610 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
22 | | eqid 2610 |
. . . 4
⊢
(Id‘(𝑂
×_{c} 𝐶)) = (Id‘(𝑂 ×_{c} 𝐶)) |
23 | | eqid 2610 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
24 | | eqid 2610 |
. . . 4
⊢
(comp‘(𝑂
×_{c} 𝐶)) = (comp‘(𝑂 ×_{c} 𝐶)) |
25 | | eqid 2610 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
26 | 16 | oppccat 16205 |
. . . . . 6
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
27 | 2, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑂 ∈ Cat) |
28 | 15, 27, 2 | xpccat 16653 |
. . . 4
⊢ (𝜑 → (𝑂 ×_{c} 𝐶) ∈ Cat) |
29 | | hofcl.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
30 | | hofcl.d |
. . . . . 6
⊢ 𝐷 = (SetCat‘𝑈) |
31 | 30 | setccat 16558 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → 𝐷 ∈ Cat) |
32 | 29, 31 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
33 | | eqid 2610 |
. . . . . . . 8
⊢
(Hom_{f} ‘𝐶) = (Hom_{f} ‘𝐶) |
34 | 33, 3 | homffn 16176 |
. . . . . . 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 5808 |
. . . . . 6
⊢
((Hom_{f} ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ ((Hom_{f}
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ∧ ran
(Hom_{f} ‘𝐶) ⊆ 𝑈)) |
38 | 35, 36, 37 | sylanbrc 695 |
. . . . 5
⊢ (𝜑 → (Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) |
39 | 30, 29 | setcbas 16551 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (Base‘𝐷)) |
40 | 39 | feq3d 5945 |
. . . . 5
⊢ (𝜑 → ((Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ (Hom_{f} ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷))) |
41 | 38, 40 | mpbid 221 |
. . . 4
⊢ (𝜑 → (Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷)) |
42 | | eqid 2610 |
. . . . . 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 6577 |
. . . . . . 7
⊢
((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∈ V |
44 | | ovex 6577 |
. . . . . . 7
⊢
((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ∈ V |
45 | 43, 44 | mpt2ex 7136 |
. . . . . 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 7128 |
. . . . 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 5895 |
. . . . 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 247 |
. . . 4
⊢ (𝜑 → (2^{nd}
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶)))) |
49 | 2 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat) |
50 | | simplrr 797 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
51 | | xp1st 7089 |
. . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
54 | | simplrl 796 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
55 | | xp1st 7089 |
. . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
58 | | xp2nd 7090 |
. . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
61 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
62 | | 1st2nd2 7096 |
. . . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
65 | 64 | oveq1d 6564 |
. . . . . . . . . . . . . 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 6566 |
. . . . . . . . . . . . 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 7090 |
. . . . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
70 | 63 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
71 | | df-ov 6552 |
. . . . . . . . . . . . . . . . 17
⊢
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
72 | 70, 71 | syl6eqr 2662 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
73 | 72 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)))) |
74 | 73 | biimpa 500 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
75 | | simplrr 797 |
. . . . . . . . . . . . . 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 16169 |
. . . . . . . . . . . . 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 2688 |
. . . . . . . . . . . 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 16169 |
. . . . . . . . . . 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 7096 |
. . . . . . . . . . . . . . 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 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
82 | | df-ov 6552 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦)) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
83 | 81, 82 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
84 | 83 | adantr 480 |
. . . . . . . . . . 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 2691 |
. . . . . . . . . 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 | | eqid 2610 |
. . . . . . . . . 10
⊢ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) = (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) |
87 | 85, 86 | fmptd 6292 |
. . . . . . . . 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 ‘𝐶)‘𝑦)) |
88 | 29 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → 𝑈 ∈ 𝑉) |
89 | 33, 3, 4, 56, 68 | homfval 16175 |
. . . . . . . . . . . 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} ‘𝑥))) |
90 | 63 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
91 | | df-ov 6552 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥)) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
92 | 90, 91 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥))) |
93 | 89, 92, 72 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘𝑥)) |
94 | 38 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (Hom_{f}
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) |
95 | 94, 54 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑥) ∈ 𝑈) |
96 | 93, 95 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) ∈ 𝑈) |
97 | 33, 3, 4, 52, 59 | homfval 16175 |
. . . . . . . . . . . 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} ‘𝑦))) |
98 | 80 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
99 | | df-ov 6552 |
. . . . . . . . . . . . 13
⊢
((1^{st} ‘𝑦)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑦)) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
100 | 98, 99 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((1^{st}
‘𝑦)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑦))) |
101 | 97, 100, 83 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘𝑦)) |
102 | 94, 50 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom_{f}
‘𝐶)‘𝑦) ∈ 𝑈) |
103 | 101, 102 | eqeltrrd 2689 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) ∈ 𝑈) |
104 | 30, 88, 21, 96, 103 | elsetchom 16554 |
. . . . . . . . 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 ‘𝐶)‘𝑦))) |
105 | 87, 104 | mpbird 246 |
. . . . . . . 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 ‘𝐶)‘𝑦))) |
106 | 93, 101 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦)) = (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) |
107 | 105, 106 | eleqtrrd 2691 |
. . . . . . 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} ‘𝐶)‘𝑦))) |
108 | 107 | ralrimivva 2954 |
. . . . . 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} ‘𝐶)‘𝑦))) |
109 | | eqid 2610 |
. . . . . . 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} ‘𝑦))𝑓))) |
110 | 109 | fmpt2 7126 |
. . . . . 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} ‘𝐶)‘𝑦))) |
111 | 108, 110 | sylib 207 |
. . . . 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} ‘𝐶)‘𝑦))) |
112 | 12 | oveqd 6566 |
. . . . . . 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} ‘𝑦))𝑓))))𝑦)) |
113 | 42 | ovmpt4g 6681 |
. . . . . . . 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} ‘𝑦))𝑓)))) |
114 | 45, 113 | mp3an3 1405 |
. . . . . . 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} ‘𝑦))𝑓)))) |
115 | 112, 114 | sylan9eq 2664 |
. . . . . 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} ‘𝑦))𝑓)))) |
116 | | eqid 2610 |
. . . . . . . 8
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
117 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
118 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
119 | 15, 18, 116, 4, 20, 117, 118 | xpchom 16643 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) = (((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
120 | 4, 16 | oppchom 16198 |
. . . . . . . 8
⊢
((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) = ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) |
121 | 120 | xpeq1i 5059 |
. . . . . . 7
⊢
(((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) = (((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
122 | 119, 121 | syl6eq 2660 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) = (((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
123 | 115, 122 | feq12d 5946 |
. . . . 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} ‘𝐶)‘𝑦)))) |
124 | 111, 123 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2^{nd} ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦)⟶(((Hom_{f}
‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom_{f} ‘𝐶)‘𝑦))) |
125 | | eqid 2610 |
. . . . . . . . . 10
⊢
(Id‘𝐶) =
(Id‘𝐶) |
126 | 2 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → 𝐶 ∈ Cat) |
127 | 55 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
128 | 127 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
129 | 67 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
130 | 129 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
131 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
132 | 3, 4, 125, 126, 128, 5, 130, 131 | catlid 16167 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (((Id‘𝐶)‘(2^{nd} ‘𝑥))(⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))𝑓) = 𝑓) |
133 | 132 | oveq1d 6564 |
. . . . . . . 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} ‘𝑥)))) |
134 | 3, 4, 125, 126, 128, 5, 130, 131 | catrid 16168 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) → (𝑓(⟨(1^{st} ‘𝑥), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑥))((Id‘𝐶)‘(1^{st} ‘𝑥))) = 𝑓) |
135 | 133, 134 | eqtrd 2644 |
. . . . . . 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} ‘𝑥))) = 𝑓) |
136 | 135 | mpteq2dva 4672 |
. . . . . 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} ‘𝑥)) ↦ 𝑓)) |
137 | | df-ov 6552 |
. . . . . . 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} ‘𝑥))⟩) |
138 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝐶 ∈ Cat) |
139 | 3, 4, 125, 138, 127 | catidcl 16166 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(1^{st} ‘𝑥)) ∈ ((1^{st}
‘𝑥)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
140 | 3, 4, 125, 138, 129 | catidcl 16166 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(2^{nd} ‘𝑥)) ∈ ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
141 | 1, 138, 3, 4, 127, 129, 127, 129, 5, 139, 140 | hof2val 16719 |
. . . . . . 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} ‘𝑥))))) |
142 | 137, 141 | syl5eqr 2658 |
. . . . . 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} ‘𝑥))))) |
143 | 62 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
144 | 143 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
145 | 144, 91 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥))) |
146 | 33, 3, 4, 127, 129 | homfval 16175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((1^{st} ‘𝑥)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑥)) =
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
147 | 145, 146 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
148 | 147 | reseq2d 5317 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Hom_{f} ‘𝐶)‘𝑥)) = ( I ↾ ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)))) |
149 | | mptresid 5375 |
. . . . . . 7
⊢ (𝑓 ∈ ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ 𝑓) = ( I ↾ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
150 | 148, 149 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Hom_{f} ‘𝐶)‘𝑥)) = (𝑓 ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) ↦ 𝑓)) |
151 | 136, 142,
150 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩(2^{nd} ‘𝑀)⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) = ( I ↾
((Hom_{f} ‘𝐶)‘𝑥))) |
152 | 143, 143 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(2^{nd} ‘𝑀)𝑥) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
153 | 143 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×_{c} 𝐶))‘𝑥) = ((Id‘(𝑂 ×_{c} 𝐶))‘⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)) |
154 | 27 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑂 ∈ Cat) |
155 | | eqid 2610 |
. . . . . . . 8
⊢
(Id‘𝑂) =
(Id‘𝑂) |
156 | 15, 154, 138, 17, 3, 155, 125, 22, 127, 129 | xpcid 16652 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×_{c} 𝐶))‘⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩) =
⟨((Id‘𝑂)‘(1^{st} ‘𝑥)), ((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
157 | 16, 125 | oppcid 16204 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) |
158 | 138, 157 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (Id‘𝑂) = (Id‘𝐶)) |
159 | 158 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝑂)‘(1^{st} ‘𝑥)) = ((Id‘𝐶)‘(1^{st}
‘𝑥))) |
160 | 159 | opeq1d 4346 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ⟨((Id‘𝑂)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩ =
⟨((Id‘𝐶)‘(1^{st} ‘𝑥)), ((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
161 | 153, 156,
160 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×_{c} 𝐶))‘𝑥) = ⟨((Id‘𝐶)‘(1^{st} ‘𝑥)), ((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩) |
162 | 152, 161 | fveq12d 6109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2^{nd} ‘𝑀)𝑥)‘((Id‘(𝑂 ×_{c} 𝐶))‘𝑥)) = ((⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)‘⟨((Id‘𝐶)‘(1^{st}
‘𝑥)),
((Id‘𝐶)‘(2^{nd} ‘𝑥))⟩)) |
163 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑈 ∈ 𝑉) |
164 | 38 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Hom_{f}
‘𝐶)‘𝑥) ∈ 𝑈) |
165 | 30, 23, 163, 164 | setcid 16559 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐷)‘((Hom_{f}
‘𝐶)‘𝑥)) = ( I ↾
((Hom_{f} ‘𝐶)‘𝑥))) |
166 | 151, 162,
165 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2^{nd} ‘𝑀)𝑥)‘((Id‘(𝑂 ×_{c} 𝐶))‘𝑥)) = ((Id‘𝐷)‘((Hom_{f}
‘𝐶)‘𝑥))) |
167 | 2 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝐶 ∈ Cat) |
168 | 29 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑈 ∈ 𝑉) |
169 | 36 | 3ad2ant1 1075 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ran (Hom_{f}
‘𝐶) ⊆ 𝑈) |
170 | | simp21 1087 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
171 | 170, 55 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
172 | 170, 67 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
173 | | simp22 1088 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
174 | 173, 51 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
175 | 173, 58 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
176 | | simp23 1089 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
177 | | xp1st 7089 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1^{st}
‘𝑧) ∈
(Base‘𝐶)) |
178 | 176, 177 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑧) ∈ (Base‘𝐶)) |
179 | | xp2nd 7090 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2^{nd}
‘𝑧) ∈
(Base‘𝐶)) |
180 | 176, 179 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑧) ∈ (Base‘𝐶)) |
181 | | simp3l 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦)) |
182 | 15, 18, 116, 4, 20, 170, 173 | xpchom 16643 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) = (((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
183 | 181, 182 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑓 ∈ (((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) |
184 | | xp1st 7089 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) → (1^{st}
‘𝑓) ∈
((1^{st} ‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦))) |
185 | 183, 184 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑓) ∈ ((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦))) |
186 | 185, 120 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑓) ∈ ((1^{st}
‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
187 | | xp2nd 7090 |
. . . . . . 7
⊢ (𝑓 ∈ (((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) → (2^{nd}
‘𝑓) ∈
((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
188 | 183, 187 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑓) ∈ ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
189 | | simp3r 1083 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧)) |
190 | 15, 18, 116, 4, 20, 173, 176 | xpchom 16643 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧) = (((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧)))) |
191 | 189, 190 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑔 ∈ (((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧)))) |
192 | | xp1st 7089 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) → (1^{st}
‘𝑔) ∈
((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧))) |
193 | 191, 192 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧))) |
194 | 4, 16 | oppchom 16198 |
. . . . . . 7
⊢
((1^{st} ‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) = ((1^{st} ‘𝑧)(Hom ‘𝐶)(1^{st} ‘𝑦)) |
195 | 193, 194 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (1^{st} ‘𝑔) ∈ ((1^{st}
‘𝑧)(Hom ‘𝐶)(1^{st} ‘𝑦))) |
196 | | xp2nd 7090 |
. . . . . . 7
⊢ (𝑔 ∈ (((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) → (2^{nd}
‘𝑔) ∈
((2^{nd} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
197 | 191, 196 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (2^{nd} ‘𝑔) ∈ ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
198 | 1, 16, 30, 167, 168, 169, 3, 4, 171, 172, 174, 175, 178, 180, 186, 188, 195, 197 | hofcllem 16721 |
. . . . 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}
‘𝑓)))) |
199 | 170, 62 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
200 | | 1st2nd2 7096 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = ⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩) |
201 | 176, 200 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑧 = ⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩) |
202 | 199, 201 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑥(2^{nd} ‘𝑀)𝑧) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)) |
203 | 173, 79 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑦 = ⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩) |
204 | 199, 203 | opeq12d 4348 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ⟨𝑥, 𝑦⟩ = ⟨⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩,
⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩⟩) |
205 | 204, 201 | oveq12d 6567 |
. . . . . . . . 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}
‘𝑧)⟩)) |
206 | | 1st2nd2 7096 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (((1^{st}
‘𝑦)(Hom ‘𝑂)(1^{st} ‘𝑧)) × ((2^{nd}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑧))) → 𝑔 = ⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩) |
207 | 191, 206 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑔 = ⟨(1^{st} ‘𝑔), (2^{nd} ‘𝑔)⟩) |
208 | | 1st2nd2 7096 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (((1^{st}
‘𝑥)(Hom ‘𝑂)(1^{st} ‘𝑦)) × ((2^{nd}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) → 𝑓 = ⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) |
209 | 183, 208 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → 𝑓 = ⟨(1^{st} ‘𝑓), (2^{nd} ‘𝑓)⟩) |
210 | 205, 207,
209 | oveq123d 6570 |
. . . . . . . 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} ‘𝑓)⟩)) |
211 | | eqid 2610 |
. . . . . . . . 9
⊢
(comp‘𝑂) =
(comp‘𝑂) |
212 | 15, 17, 3, 116, 4, 171, 172, 174, 175, 211, 5, 24, 178, 180, 185, 188, 193, 197 | xpcco2 16650 |
. . . . . . . 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} ‘𝑓))⟩) |
213 | 3, 5, 16, 171, 174, 178 | oppcco 16200 |
. . . . . . . . 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} ‘𝑔))) |
214 | 213 | opeq1d 4346 |
. . . . . . . 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} ‘𝑓))⟩) |
215 | 210, 212,
214 | 3eqtrd 2648 |
. . . . . . 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} ‘𝑓))⟩) |
216 | 202, 215 | fveq12d 6109 |
. . . . . 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} ‘𝑓))⟩)) |
217 | | df-ov 6552 |
. . . . . 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} ‘𝑓))⟩) |
218 | 216, 217 | syl6eqr 2662 |
. . . . 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} ‘𝑓)))) |
219 | 199 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
220 | 219, 91 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑥))) |
221 | 33, 3, 4, 171, 172 | homfval 16175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑥)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑥)) =
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
222 | 220, 221 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑥) = ((1^{st}
‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
223 | 203 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
224 | 223, 99 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((1^{st}
‘𝑦)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑦))) |
225 | 33, 3, 4, 174, 175 | homfval 16175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑦)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑦)) =
((1^{st} ‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
226 | 224, 225 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑦) = ((1^{st}
‘𝑦)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
227 | 222, 226 | opeq12d 4348 |
. . . . . . 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} ‘𝑦))⟩) |
228 | 201 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑧) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)) |
229 | | df-ov 6552 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑧)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑧)) = ((Hom_{f}
‘𝐶)‘⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩) |
230 | 228, 229 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑧) = ((1^{st}
‘𝑧)(Hom_{f} ‘𝐶)(2^{nd} ‘𝑧))) |
231 | 33, 3, 4, 178, 180 | homfval 16175 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((1^{st} ‘𝑧)(Hom_{f}
‘𝐶)(2^{nd}
‘𝑧)) =
((1^{st} ‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
232 | 230, 231 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → ((Hom_{f}
‘𝐶)‘𝑧) = ((1^{st}
‘𝑧)(Hom ‘𝐶)(2^{nd} ‘𝑧))) |
233 | 227, 232 | oveq12d 6567 |
. . . . . 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} ‘𝑧)))) |
234 | 203, 201 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑦(2^{nd} ‘𝑀)𝑧) = (⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑧), (2^{nd} ‘𝑧)⟩)) |
235 | 234, 207 | fveq12d 6109 |
. . . . . . 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}
‘𝑔)⟩)) |
236 | | df-ov 6552 |
. . . . . . 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}
‘𝑔)⟩) |
237 | 235, 236 | syl6eqr 2662 |
. . . . . 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} ‘𝑔))) |
238 | 199, 203 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×_{c} 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×_{c} 𝐶))𝑧))) → (𝑥(2^{nd} ‘𝑀)𝑦) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(2^{nd}
‘𝑀)⟨(1^{st} ‘𝑦), (2^{nd} ‘𝑦)⟩)) |
239 | 238, 209 | fveq12d 6109 |
. . . . . . 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}
‘𝑓)⟩)) |
240 | | df-ov 6552 |
. . . . . . 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}
‘𝑓)⟩) |
241 | 239, 240 | syl6eqr 2662 |
. . . . . 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} ‘𝑓))) |
242 | 233, 237,
241 | oveq123d 6570 |
. . . . 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}
‘𝑓)))) |
243 | 198, 218,
242 | 3eqtr4d 2654 |
. . . 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} ‘𝑀)𝑦)‘𝑓))) |
244 | 18, 19, 20, 21, 22, 23, 24, 25, 28, 32, 41, 48, 124, 166, 243 | isfuncd 16348 |
. . 3
⊢ (𝜑 → (Hom_{f}
‘𝐶)((𝑂 ×_{c}
𝐶) Func 𝐷)(2^{nd} ‘𝑀)) |
245 | | df-br 4584 |
. . 3
⊢
((Hom_{f} ‘𝐶)((𝑂 ×_{c} 𝐶) Func 𝐷)(2^{nd} ‘𝑀) ↔ ⟨(Hom_{f}
‘𝐶), (2^{nd}
‘𝑀)⟩ ∈
((𝑂
×_{c} 𝐶) Func 𝐷)) |
246 | 244, 245 | sylib 207 |
. 2
⊢ (𝜑 →
⟨(Hom_{f} ‘𝐶), (2^{nd} ‘𝑀)⟩ ∈ ((𝑂 ×_{c} 𝐶) Func 𝐷)) |
247 | 14, 246 | eqeltrd 2688 |
1
⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×_{c} 𝐶) Func 𝐷)) |