Step | Hyp | Ref
| Expression |
1 | | hofcl.m |
. . . 4
⊢ 𝑀 =
(HomF‘𝐶) |
2 | | hofcl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
3 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
4 | | eqid 2622 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
5 | | eqid 2622 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
6 | 1, 2, 3, 4, 5 | hofval 16892 |
. . 3
⊢ (𝜑 → 𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉) |
7 | | fvex 6201 |
. . . . . 6
⊢
(Homf ‘𝐶) ∈ V |
8 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
9 | 8, 8 | xpex 6962 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐶))
∈ V |
10 | 9, 9 | mpt2ex 7247 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) ∈ V |
11 | 7, 10 | op2ndd 7179 |
. . . . 5
⊢ (𝑀 = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉 → (2nd
‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))) |
12 | 6, 11 | syl 17 |
. . . 4
⊢ (𝜑 → (2nd
‘𝑀) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))) |
13 | 12 | opeq2d 4409 |
. . 3
⊢ (𝜑 →
〈(Homf ‘𝐶), (2nd ‘𝑀)〉 = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉) |
14 | 6, 13 | eqtr4d 2659 |
. 2
⊢ (𝜑 → 𝑀 = 〈(Homf
‘𝐶), (2nd
‘𝑀)〉) |
15 | | eqid 2622 |
. . . . 5
⊢ (𝑂 ×c
𝐶) = (𝑂 ×c 𝐶) |
16 | | hofcl.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
17 | 16, 3 | oppcbas 16378 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝑂) |
18 | 15, 17, 3 | xpcbas 16818 |
. . . 4
⊢
((Base‘𝐶)
× (Base‘𝐶)) =
(Base‘(𝑂
×c 𝐶)) |
19 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
20 | | eqid 2622 |
. . . 4
⊢ (Hom
‘(𝑂
×c 𝐶)) = (Hom ‘(𝑂 ×c 𝐶)) |
21 | | eqid 2622 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
22 | | eqid 2622 |
. . . 4
⊢
(Id‘(𝑂
×c 𝐶)) = (Id‘(𝑂 ×c 𝐶)) |
23 | | eqid 2622 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
24 | | eqid 2622 |
. . . 4
⊢
(comp‘(𝑂
×c 𝐶)) = (comp‘(𝑂 ×c 𝐶)) |
25 | | eqid 2622 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
26 | 16 | oppccat 16382 |
. . . . . 6
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
27 | 2, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑂 ∈ Cat) |
28 | 15, 27, 2 | xpccat 16830 |
. . . 4
⊢ (𝜑 → (𝑂 ×c 𝐶) ∈ Cat) |
29 | | hofcl.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
30 | | hofcl.d |
. . . . . 6
⊢ 𝐷 = (SetCat‘𝑈) |
31 | 30 | setccat 16735 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → 𝐷 ∈ Cat) |
32 | 29, 31 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
33 | | eqid 2622 |
. . . . . . . 8
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) |
34 | 33, 3 | homffn 16353 |
. . . . . . 7
⊢
(Homf ‘𝐶) Fn ((Base‘𝐶) × (Base‘𝐶)) |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (Homf
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
36 | | hofcl.h |
. . . . . 6
⊢ (𝜑 → ran
(Homf ‘𝐶) ⊆ 𝑈) |
37 | | df-f 5892 |
. . . . . 6
⊢
((Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ ((Homf
‘𝐶) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ∧ ran
(Homf ‘𝐶) ⊆ 𝑈)) |
38 | 35, 36, 37 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → (Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) |
39 | 30, 29 | setcbas 16728 |
. . . . . 6
⊢ (𝜑 → 𝑈 = (Base‘𝐷)) |
40 | 39 | feq3d 6032 |
. . . . 5
⊢ (𝜑 → ((Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈 ↔ (Homf ‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷))) |
41 | 38, 40 | mpbid 222 |
. . . 4
⊢ (𝜑 → (Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶(Base‘𝐷)) |
42 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) |
43 | | ovex 6678 |
. . . . . . 7
⊢
((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∈ V |
44 | | ovex 6678 |
. . . . . . 7
⊢
((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ∈ V |
45 | 43, 44 | mpt2ex 7247 |
. . . . . 6
⊢ (𝑓 ∈ ((1st
‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) ∈ V |
46 | 42, 45 | fnmpt2i 7239 |
. . . . 5
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))) |
47 | 12 | fneq1d 5981 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶))) ↔
(𝑥 ∈
((Base‘𝐶) ×
(Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) Fn (((Base‘𝐶) × (Base‘𝐶)) × ((Base‘𝐶) × (Base‘𝐶))))) |
48 | 46, 47 | mpbiri 248 |
. . . 4
⊢ (𝜑 → (2nd
‘𝑀) Fn
(((Base‘𝐶) ×
(Base‘𝐶)) ×
((Base‘𝐶) ×
(Base‘𝐶)))) |
49 | 2 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat) |
50 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
51 | | xp1st 7198 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑦) ∈
(Base‘𝐶)) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (1st ‘𝑦) ∈ (Base‘𝐶)) |
53 | 52 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑦) ∈ (Base‘𝐶)) |
54 | | simplrl 800 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
55 | | xp1st 7198 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑥) ∈
(Base‘𝐶)) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
57 | 56 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
58 | | xp2nd 7199 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑦) ∈
(Base‘𝐶)) |
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (2nd ‘𝑦) ∈ (Base‘𝐶)) |
60 | 59 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑦) ∈ (Base‘𝐶)) |
61 | | simplrl 800 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))) |
62 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
63 | 54, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
65 | 64 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2nd ‘𝑦)) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))) |
66 | 65 | oveqd 6667 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) = (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ)) |
67 | | xp2nd 7199 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑥) ∈
(Base‘𝐶)) |
68 | 54, 67 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
70 | 63 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
71 | | df-ov 6653 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
72 | 70, 71 | syl6eqr 2674 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
73 | 72 | eleq2d 2687 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))) |
74 | 73 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
75 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
76 | 3, 4, 5, 49, 57, 69, 60, 74, 75 | catcocl 16346 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
77 | 66, 76 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
78 | 3, 4, 5, 49, 53, 57, 60, 61, 77 | catcocl 16346 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓) ∈ ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) |
79 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
80 | 50, 79 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
81 | 80 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
82 | | df-ov 6653 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦)) = ((Hom ‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
83 | 81, 82 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) |
84 | 83 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((Hom ‘𝐶)‘𝑦) = ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) |
85 | 78, 84 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓) ∈ ((Hom ‘𝐶)‘𝑦)) |
86 | | eqid 2622 |
. . . . . . . . . 10
⊢ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) = (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) |
87 | 85, 86 | fmptd 6385 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦)) |
88 | 29 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → 𝑈 ∈ 𝑉) |
89 | 33, 3, 4, 56, 68 | homfval 16352 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((1st ‘𝑥)(Homf
‘𝐶)(2nd
‘𝑥)) =
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
90 | 63 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
91 | | df-ov 6653 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥)) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
92 | 90, 91 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥))) |
93 | 89, 92, 72 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘𝑥)) |
94 | 38 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (Homf
‘𝐶):((Base‘𝐶) × (Base‘𝐶))⟶𝑈) |
95 | 94, 54 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑥) ∈ 𝑈) |
96 | 93, 95 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) ∈ 𝑈) |
97 | 33, 3, 4, 52, 59 | homfval 16352 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((1st ‘𝑦)(Homf
‘𝐶)(2nd
‘𝑦)) =
((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) |
98 | 80 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) = ((Homf
‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
99 | | df-ov 6653 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦)) = ((Homf
‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
100 | 98, 99 | syl6eqr 2674 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) = ((1st
‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦))) |
101 | 97, 100, 83 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) = ((Hom ‘𝐶)‘𝑦)) |
102 | 94, 50 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Homf
‘𝐶)‘𝑦) ∈ 𝑈) |
103 | 101, 102 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑦) ∈ 𝑈) |
104 | 30, 88, 21, 96, 103 | elsetchom 16731 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦)) ↔ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)):((Hom ‘𝐶)‘𝑥)⟶((Hom ‘𝐶)‘𝑦))) |
105 | 87, 104 | mpbird 247 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) |
106 | 93, 101 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) = (((Hom ‘𝐶)‘𝑥)(Hom ‘𝐷)((Hom ‘𝐶)‘𝑦))) |
107 | 105, 106 | eleqtrrd 2704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) |
108 | 107 | ralrimivva 2971 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ∀𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))∀𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) |
109 | | eqid 2622 |
. . . . . . 7
⊢ (𝑓 ∈ ((1st
‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) |
110 | 109 | fmpt2 7237 |
. . . . . 6
⊢
(∀𝑓 ∈
((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))∀𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))(ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) ∈ (((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) |
111 | 108, 110 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) |
112 | 12 | oveqd 6667 |
. . . . . . 7
⊢ (𝜑 → (𝑥(2nd ‘𝑀)𝑦) = (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦)) |
113 | 42 | ovmpt4g 6783 |
. . . . . . . 8
⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) ∈ V) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) |
114 | 45, 113 | mp3an3 1413 |
. . . . . . 7
⊢ ((𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) |
115 | 112, 114 | sylan9eq 2676 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd ‘𝑀)𝑦) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) |
116 | | eqid 2622 |
. . . . . . . 8
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
117 | | simprl 794 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
118 | | simprr 796 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
119 | 15, 18, 116, 4, 20, 117, 118 | xpchom 16820 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) |
120 | 4, 16 | oppchom 16375 |
. . . . . . . 8
⊢
((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) = ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) |
121 | 120 | xpeq1i 5135 |
. . . . . . 7
⊢
(((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) = (((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
122 | 119, 121 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) |
123 | 115, 122 | feq12d 6033 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((𝑥(2nd ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)) ↔ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))):(((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦)))) |
124 | 111, 123 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑥(2nd ‘𝑀)𝑦):(𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)⟶(((Homf
‘𝐶)‘𝑥)(Hom ‘𝐷)((Homf ‘𝐶)‘𝑦))) |
125 | | eqid 2622 |
. . . . . . . . . 10
⊢
(Id‘𝐶) =
(Id‘𝐶) |
126 | 2 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → 𝐶 ∈ Cat) |
127 | 55 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
128 | 127 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
129 | 67 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
130 | 129 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
131 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
132 | 3, 4, 125, 126, 128, 5, 130, 131 | catlid 16344 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓) = 𝑓) |
133 | 132 | oveq1d 6665 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = (𝑓(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))) |
134 | 3, 4, 125, 126, 128, 5, 130, 131 | catrid 16345 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → (𝑓(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = 𝑓) |
135 | 133, 134 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ 𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) → ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))) = 𝑓) |
136 | 135 | mpteq2dva 4744 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥)))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓)) |
137 | | df-ov 6653 |
. . . . . . 7
⊢
(((Id‘𝐶)‘(1st ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)((Id‘𝐶)‘(2nd ‘𝑥))) = ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉) |
138 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝐶 ∈ Cat) |
139 | 3, 4, 125, 138, 127 | catidcl 16343 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(1st ‘𝑥)) ∈ ((1st
‘𝑥)(Hom ‘𝐶)(1st ‘𝑥))) |
140 | 3, 4, 125, 138, 129 | catidcl 16343 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐶)‘(2nd ‘𝑥)) ∈ ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
141 | 1, 138, 3, 4, 127, 129, 127, 129, 5, 139, 140 | hof2val 16896 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (((Id‘𝐶)‘(1st ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)((Id‘𝐶)‘(2nd ‘𝑥))) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))))) |
142 | 137, 141 | syl5eqr 2670 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ ((((Id‘𝐶)‘(2nd ‘𝑥))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))𝑓)(〈(1st ‘𝑥), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑥))((Id‘𝐶)‘(1st ‘𝑥))))) |
143 | 62 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
144 | 143 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
145 | 144, 91 | syl6eqr 2674 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥))) |
146 | 33, 3, 4, 127, 129 | homfval 16352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((1st ‘𝑥)(Homf
‘𝐶)(2nd
‘𝑥)) =
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
147 | 145, 146 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
148 | 147 | reseq2d 5396 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Homf ‘𝐶)‘𝑥)) = ( I ↾ ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))) |
149 | | mptresid 5456 |
. . . . . . 7
⊢ (𝑓 ∈ ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓) = ( I ↾ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
150 | 148, 149 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ( I ↾
((Homf ‘𝐶)‘𝑥)) = (𝑓 ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) ↦ 𝑓)) |
151 | 136, 142,
150 | 3eqtr4d 2666 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑥), (2nd
‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉) = ( I ↾
((Homf ‘𝐶)‘𝑥))) |
152 | 143, 143 | oveq12d 6668 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (𝑥(2nd ‘𝑀)𝑥) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
153 | 143 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = ((Id‘(𝑂 ×c 𝐶))‘〈(1st
‘𝑥), (2nd
‘𝑥)〉)) |
154 | 27 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑂 ∈ Cat) |
155 | | eqid 2622 |
. . . . . . . 8
⊢
(Id‘𝑂) =
(Id‘𝑂) |
156 | 15, 154, 138, 17, 3, 155, 125, 22, 127, 129 | xpcid 16829 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘〈(1st
‘𝑥), (2nd
‘𝑥)〉) =
〈((Id‘𝑂)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))〉) |
157 | 16, 125 | oppcid 16381 |
. . . . . . . . . 10
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) |
158 | 138, 157 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → (Id‘𝑂) = (Id‘𝐶)) |
159 | 158 | fveq1d 6193 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝑂)‘(1st ‘𝑥)) = ((Id‘𝐶)‘(1st
‘𝑥))) |
160 | 159 | opeq1d 4408 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 〈((Id‘𝑂)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉 =
〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))〉) |
161 | 153, 156,
160 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘(𝑂 ×c 𝐶))‘𝑥) = 〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐶)‘(2nd ‘𝑥))〉) |
162 | 152, 161 | fveq12d 6197 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd ‘𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑥), (2nd ‘𝑥)〉)‘〈((Id‘𝐶)‘(1st
‘𝑥)),
((Id‘𝐶)‘(2nd ‘𝑥))〉)) |
163 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → 𝑈 ∈ 𝑉) |
164 | 38 | ffvelrnda 6359 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Homf
‘𝐶)‘𝑥) ∈ 𝑈) |
165 | 30, 23, 163, 164 | setcid 16736 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Id‘𝐷)‘((Homf
‘𝐶)‘𝑥)) = ( I ↾
((Homf ‘𝐶)‘𝑥))) |
166 | 151, 162,
165 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((𝑥(2nd ‘𝑀)𝑥)‘((Id‘(𝑂 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((Homf
‘𝐶)‘𝑥))) |
167 | 2 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat) |
168 | 29 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑈 ∈ 𝑉) |
169 | 36 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ran (Homf
‘𝐶) ⊆ 𝑈) |
170 | | simp21 1094 |
. . . . . . 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 𝐶))𝑧))) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
172 | 170, 67 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
173 | | simp22 1095 |
. . . . . . 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 𝐶))𝑧))) → (1st ‘𝑦) ∈ (Base‘𝐶)) |
175 | 173, 58 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑦) ∈ (Base‘𝐶)) |
176 | | simp23 1096 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) |
177 | | xp1st 7198 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑧) ∈
(Base‘𝐶)) |
178 | 176, 177 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑧) ∈ (Base‘𝐶)) |
179 | | xp2nd 7199 |
. . . . . . 7
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑧) ∈
(Base‘𝐶)) |
180 | 176, 179 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑧) ∈ (Base‘𝐶)) |
181 | | simp3l 1089 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦)) |
182 | 15, 18, 116, 4, 20, 170, 173 | xpchom 16820 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) = (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) |
183 | 181, 182 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) |
184 | | xp1st 7198 |
. . . . . . . 8
⊢ (𝑓 ∈ (((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → (1st
‘𝑓) ∈
((1st ‘𝑥)(Hom ‘𝑂)(1st ‘𝑦))) |
185 | 183, 184 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑓) ∈ ((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦))) |
186 | 185, 120 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑓) ∈ ((1st
‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))) |
187 | | xp2nd 7199 |
. . . . . . 7
⊢ (𝑓 ∈ (((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → (2nd
‘𝑓) ∈
((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
188 | 183, 187 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑓) ∈ ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
189 | | simp3r 1090 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧)) |
190 | 15, 18, 116, 4, 20, 173, 176 | xpchom 16820 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧) = (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) |
191 | 189, 190 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) |
192 | | xp1st 7198 |
. . . . . . . 8
⊢ (𝑔 ∈ (((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → (1st
‘𝑔) ∈
((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧))) |
193 | 191, 192 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑔) ∈ ((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧))) |
194 | 4, 16 | oppchom 16375 |
. . . . . . 7
⊢
((1st ‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) = ((1st ‘𝑧)(Hom ‘𝐶)(1st ‘𝑦)) |
195 | 193, 194 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (1st ‘𝑔) ∈ ((1st
‘𝑧)(Hom ‘𝐶)(1st ‘𝑦))) |
196 | | xp2nd 7199 |
. . . . . . 7
⊢ (𝑔 ∈ (((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → (2nd
‘𝑔) ∈
((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) |
197 | 191, 196 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (2nd ‘𝑔) ∈ ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) |
198 | 1, 16, 30, 167, 168, 169, 3, 4, 171, 172, 174, 175, 178, 180, 186, 188, 195, 197 | hofcllem 16898 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))) = (((1st
‘𝑔)(〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)(2nd
‘𝑔))(〈((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))((1st ‘𝑓)(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)(2nd
‘𝑓)))) |
199 | 170, 62 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
200 | | 1st2nd2 7205 |
. . . . . . . . 9
⊢ (𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
201 | 176, 200 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
202 | 199, 201 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝑀)𝑧) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
203 | 173, 79 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) |
204 | 199, 203 | opeq12d 4410 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 〈𝑥, 𝑦〉 = 〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉) |
205 | 204, 201 | oveq12d 6668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧) = (〈〈(1st ‘𝑥), (2nd ‘𝑥)〉, 〈(1st
‘𝑦), (2nd
‘𝑦)〉〉(comp‘(𝑂 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)) |
206 | | 1st2nd2 7205 |
. . . . . . . . . 10
⊢ (𝑔 ∈ (((1st
‘𝑦)(Hom ‘𝑂)(1st ‘𝑧)) × ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
207 | 191, 206 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) |
208 | | 1st2nd2 7205 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (((1st
‘𝑥)(Hom ‘𝑂)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
209 | 183, 208 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) |
210 | 205, 207,
209 | oveq123d 6671 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓) = (〈(1st ‘𝑔), (2nd ‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑂 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉)) |
211 | | eqid 2622 |
. . . . . . . . 9
⊢
(comp‘𝑂) =
(comp‘𝑂) |
212 | 15, 17, 3, 116, 4, 171, 172, 174, 175, 211, 5, 24, 178, 180, 185, 188, 193, 197 | xpcco2 16827 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (〈(1st
‘𝑔), (2nd
‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑂 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉) =
〈((1st ‘𝑔)(〈(1st ‘𝑥), (1st ‘𝑦)〉(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) |
213 | 3, 5, 16, 171, 174, 178 | oppcco 16377 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑔)(〈(1st
‘𝑥), (1st
‘𝑦)〉(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)) = ((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))) |
214 | 213 | opeq1d 4408 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 〈((1st
‘𝑔)(〈(1st ‘𝑥), (1st ‘𝑦)〉(comp‘𝑂)(1st ‘𝑧))(1st ‘𝑓)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉 =
〈((1st ‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) |
215 | 210, 212,
214 | 3eqtrd 2660 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓) = 〈((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) |
216 | 202, 215 | fveq12d 6197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈((1st
‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉)) |
217 | | df-ov 6653 |
. . . . . 6
⊢
(((1st ‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈((1st
‘𝑓)(〈(1st ‘𝑧), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔)), ((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓))〉) |
218 | 216, 217 | syl6eqr 2674 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((1st ‘𝑓)(〈(1st
‘𝑧), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑥))(1st ‘𝑔))(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)((2nd
‘𝑔)(〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐶)(2nd ‘𝑧))(2nd ‘𝑓)))) |
219 | 199 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑥) = ((Homf
‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
220 | 219, 91 | syl6eqr 2674 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Homf ‘𝐶)(2nd ‘𝑥))) |
221 | 33, 3, 4, 171, 172 | homfval 16352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑥)(Homf
‘𝐶)(2nd
‘𝑥)) =
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
222 | 220, 221 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑥) = ((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
223 | 203 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑦) = ((Homf
‘𝐶)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
224 | 223, 99 | syl6eqr 2674 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑦) = ((1st
‘𝑦)(Homf ‘𝐶)(2nd ‘𝑦))) |
225 | 33, 3, 4, 174, 175 | homfval 16352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑦)(Homf
‘𝐶)(2nd
‘𝑦)) =
((1st ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) |
226 | 224, 225 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑦) = ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))) |
227 | 222, 226 | opeq12d 4410 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → 〈((Homf
‘𝐶)‘𝑥), ((Homf
‘𝐶)‘𝑦)〉 = 〈((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉) |
228 | 201 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑧) = ((Homf
‘𝐶)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
229 | | df-ov 6653 |
. . . . . . . . 9
⊢
((1st ‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧)) = ((Homf
‘𝐶)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
230 | 228, 229 | syl6eqr 2674 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑧) = ((1st
‘𝑧)(Homf ‘𝐶)(2nd ‘𝑧))) |
231 | 33, 3, 4, 178, 180 | homfval 16352 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((1st ‘𝑧)(Homf
‘𝐶)(2nd
‘𝑧)) =
((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧))) |
232 | 230, 231 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((Homf
‘𝐶)‘𝑧) = ((1st
‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧))) |
233 | 227, 232 | oveq12d 6668 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (〈((Homf
‘𝐶)‘𝑥), ((Homf
‘𝐶)‘𝑦)〉(comp‘𝐷)((Homf
‘𝐶)‘𝑧)) = (〈((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))) |
234 | 203, 201 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑦(2nd ‘𝑀)𝑧) = (〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
235 | 234, 207 | fveq12d 6197 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝑀)𝑧)‘𝑔) = ((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) |
236 | | df-ov 6653 |
. . . . . . 7
⊢
((1st ‘𝑔)(〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝑀)〈(1st ‘𝑧), (2nd ‘𝑧)〉)(2nd
‘𝑔)) =
((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉) |
237 | 235, 236 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝑀)𝑧)‘𝑔) = ((1st ‘𝑔)(〈(1st
‘𝑦), (2nd
‘𝑦)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)(2nd ‘𝑔))) |
238 | 199, 203 | oveq12d 6668 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝑀)𝑦) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)) |
239 | 238, 209 | fveq12d 6197 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑦)‘𝑓) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉)) |
240 | | df-ov 6653 |
. . . . . . 7
⊢
((1st ‘𝑓)(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)(2nd
‘𝑓)) =
((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑦), (2nd
‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉) |
241 | 239, 240 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑦)‘𝑓) = ((1st ‘𝑓)(〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝑀)〈(1st
‘𝑦), (2nd
‘𝑦)〉)(2nd ‘𝑓))) |
242 | 233, 237,
241 | oveq123d 6671 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → (((𝑦(2nd ‘𝑀)𝑧)‘𝑔)(〈((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)〉(comp‘𝐷)((Homf ‘𝐶)‘𝑧))((𝑥(2nd ‘𝑀)𝑦)‘𝑓)) = (((1st ‘𝑔)(〈(1st
‘𝑦), (2nd
‘𝑦)〉(2nd ‘𝑀)〈(1st
‘𝑧), (2nd
‘𝑧)〉)(2nd ‘𝑔))(〈((1st
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)), ((1st
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑧)(Hom ‘𝐶)(2nd ‘𝑧)))((1st ‘𝑓)(〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝑀)〈(1st ‘𝑦), (2nd ‘𝑦)〉)(2nd
‘𝑓)))) |
243 | 198, 218,
242 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑂 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑂 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝑀)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑂 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd ‘𝑀)𝑧)‘𝑔)(〈((Homf ‘𝐶)‘𝑥), ((Homf ‘𝐶)‘𝑦)〉(comp‘𝐷)((Homf ‘𝐶)‘𝑧))((𝑥(2nd ‘𝑀)𝑦)‘𝑓))) |
244 | 18, 19, 20, 21, 22, 23, 24, 25, 28, 32, 41, 48, 124, 166, 243 | isfuncd 16525 |
. . 3
⊢ (𝜑 → (Homf
‘𝐶)((𝑂 ×c
𝐶) Func 𝐷)(2nd ‘𝑀)) |
245 | | df-br 4654 |
. . 3
⊢
((Homf ‘𝐶)((𝑂 ×c 𝐶) Func 𝐷)(2nd ‘𝑀) ↔ 〈(Homf
‘𝐶), (2nd
‘𝑀)〉 ∈
((𝑂
×c 𝐶) Func 𝐷)) |
246 | 244, 245 | sylib 208 |
. 2
⊢ (𝜑 →
〈(Homf ‘𝐶), (2nd ‘𝑀)〉 ∈ ((𝑂 ×c 𝐶) Func 𝐷)) |
247 | 14, 246 | eqeltrd 2701 |
1
⊢ (𝜑 → 𝑀 ∈ ((𝑂 ×c 𝐶) Func 𝐷)) |