Step | Hyp | Ref
| Expression |
1 | | funcoppc.o |
. . 3
⊢ 𝑂 = (oppCat‘𝐶) |
2 | | eqid 2622 |
. . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | 1, 2 | oppcbas 16378 |
. 2
⊢
(Base‘𝐶) =
(Base‘𝑂) |
4 | | funcoppc.p |
. . 3
⊢ 𝑃 = (oppCat‘𝐷) |
5 | | eqid 2622 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
6 | 4, 5 | oppcbas 16378 |
. 2
⊢
(Base‘𝐷) =
(Base‘𝑃) |
7 | | eqid 2622 |
. 2
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
8 | | eqid 2622 |
. 2
⊢ (Hom
‘𝑃) = (Hom
‘𝑃) |
9 | | eqid 2622 |
. 2
⊢
(Id‘𝑂) =
(Id‘𝑂) |
10 | | eqid 2622 |
. 2
⊢
(Id‘𝑃) =
(Id‘𝑃) |
11 | | eqid 2622 |
. 2
⊢
(comp‘𝑂) =
(comp‘𝑂) |
12 | | eqid 2622 |
. 2
⊢
(comp‘𝑃) =
(comp‘𝑃) |
13 | | funcoppc.f |
. . . . . 6
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) |
14 | | df-br 4654 |
. . . . . 6
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
15 | 13, 14 | sylib 208 |
. . . . 5
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) |
16 | | funcrcl 16523 |
. . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
18 | 17 | simpld 475 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
19 | 1 | oppccat 16382 |
. . 3
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
20 | 18, 19 | syl 17 |
. 2
⊢ (𝜑 → 𝑂 ∈ Cat) |
21 | 17 | simprd 479 |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
22 | 4 | oppccat 16382 |
. . 3
⊢ (𝐷 ∈ Cat → 𝑃 ∈ Cat) |
23 | 21, 22 | syl 17 |
. 2
⊢ (𝜑 → 𝑃 ∈ Cat) |
24 | 2, 5, 13 | funcf1 16526 |
. 2
⊢ (𝜑 → 𝐹:(Base‘𝐶)⟶(Base‘𝐷)) |
25 | 2, 13 | funcfn2 16529 |
. . 3
⊢ (𝜑 → 𝐺 Fn ((Base‘𝐶) × (Base‘𝐶))) |
26 | | tposfn 7381 |
. . 3
⊢ (𝐺 Fn ((Base‘𝐶) × (Base‘𝐶)) → tpos 𝐺 Fn ((Base‘𝐶) × (Base‘𝐶))) |
27 | 25, 26 | syl 17 |
. 2
⊢ (𝜑 → tpos 𝐺 Fn ((Base‘𝐶) × (Base‘𝐶))) |
28 | | eqid 2622 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
29 | | eqid 2622 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
30 | 13 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹(𝐶 Func 𝐷)𝐺) |
31 | | simprr 796 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
32 | | simprl 794 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
33 | 2, 28, 29, 30, 31, 32 | funcf2 16528 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑦𝐺𝑥):(𝑦(Hom ‘𝐶)𝑥)⟶((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥))) |
34 | | ovtpos 7367 |
. . . . 5
⊢ (𝑥tpos 𝐺𝑦) = (𝑦𝐺𝑥) |
35 | 34 | feq1i 6036 |
. . . 4
⊢ ((𝑥tpos 𝐺𝑦):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) ↔ (𝑦𝐺𝑥):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦))) |
36 | 28, 1 | oppchom 16375 |
. . . . 5
⊢ (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥) |
37 | 29, 4 | oppchom 16375 |
. . . . 5
⊢ ((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) = ((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥)) |
38 | 36, 37 | feq23i 6039 |
. . . 4
⊢ ((𝑦𝐺𝑥):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) ↔ (𝑦𝐺𝑥):(𝑦(Hom ‘𝐶)𝑥)⟶((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥))) |
39 | 35, 38 | bitri 264 |
. . 3
⊢ ((𝑥tpos 𝐺𝑦):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) ↔ (𝑦𝐺𝑥):(𝑦(Hom ‘𝐶)𝑥)⟶((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥))) |
40 | 33, 39 | sylibr 224 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥tpos 𝐺𝑦):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦))) |
41 | | eqid 2622 |
. . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) |
42 | | eqid 2622 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
43 | 13 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹(𝐶 Func 𝐷)𝐺) |
44 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
45 | 2, 41, 42, 43, 44 | funcid 16530 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥))) |
46 | | ovtpos 7367 |
. . . . 5
⊢ (𝑥tpos 𝐺𝑥) = (𝑥𝐺𝑥) |
47 | 46 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥tpos 𝐺𝑥) = (𝑥𝐺𝑥)) |
48 | 1, 41 | oppcid 16381 |
. . . . . . 7
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) |
49 | 18, 48 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Id‘𝑂) = (Id‘𝐶)) |
50 | 49 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Id‘𝑂) = (Id‘𝐶)) |
51 | 50 | fveq1d 6193 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑂)‘𝑥) = ((Id‘𝐶)‘𝑥)) |
52 | 47, 51 | fveq12d 6197 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥tpos 𝐺𝑥)‘((Id‘𝑂)‘𝑥)) = ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥))) |
53 | 4, 42 | oppcid 16381 |
. . . . . 6
⊢ (𝐷 ∈ Cat →
(Id‘𝑃) =
(Id‘𝐷)) |
54 | 21, 53 | syl 17 |
. . . . 5
⊢ (𝜑 → (Id‘𝑃) = (Id‘𝐷)) |
55 | 54 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Id‘𝑃) = (Id‘𝐷)) |
56 | 55 | fveq1d 6193 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑃)‘(𝐹‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥))) |
57 | 45, 52, 56 | 3eqtr4d 2666 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥tpos 𝐺𝑥)‘((Id‘𝑂)‘𝑥)) = ((Id‘𝑃)‘(𝐹‘𝑥))) |
58 | | eqid 2622 |
. . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) |
59 | | eqid 2622 |
. . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) |
60 | 13 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝐹(𝐶 Func 𝐷)𝐺) |
61 | | simp23 1096 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑧 ∈ (Base‘𝐶)) |
62 | | simp22 1095 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑦 ∈ (Base‘𝐶)) |
63 | | simp21 1094 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑥 ∈ (Base‘𝐶)) |
64 | | simp3r 1090 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧)) |
65 | 28, 1 | oppchom 16375 |
. . . . . 6
⊢ (𝑦(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑦) |
66 | 64, 65 | syl6eleq 2711 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑦)) |
67 | | simp3l 1089 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦)) |
68 | 67, 36 | syl6eleq 2711 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) |
69 | 2, 28, 58, 59, 60, 61, 62, 63, 66, 68 | funcco 16531 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑧𝐺𝑥)‘(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) = (((𝑦𝐺𝑥)‘𝑓)(〈(𝐹‘𝑧), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑥))((𝑧𝐺𝑦)‘𝑔))) |
70 | 2, 58, 1, 63, 62, 61 | oppcco 16377 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) = (𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) |
71 | 70 | fveq2d 6195 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑧𝐺𝑥)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = ((𝑧𝐺𝑥)‘(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔))) |
72 | 24 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝐹:(Base‘𝐶)⟶(Base‘𝐷)) |
73 | 72, 63 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝐹‘𝑥) ∈ (Base‘𝐷)) |
74 | 72, 62 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝐹‘𝑦) ∈ (Base‘𝐷)) |
75 | 72, 61 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝐹‘𝑧) ∈ (Base‘𝐷)) |
76 | 5, 59, 4, 73, 74, 75 | oppcco 16377 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (((𝑧𝐺𝑦)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑦𝐺𝑥)‘𝑓)) = (((𝑦𝐺𝑥)‘𝑓)(〈(𝐹‘𝑧), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑥))((𝑧𝐺𝑦)‘𝑔))) |
77 | 69, 71, 76 | 3eqtr4d 2666 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑧𝐺𝑥)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = (((𝑧𝐺𝑦)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑦𝐺𝑥)‘𝑓))) |
78 | | ovtpos 7367 |
. . . 4
⊢ (𝑥tpos 𝐺𝑧) = (𝑧𝐺𝑥) |
79 | 78 | fveq1i 6192 |
. . 3
⊢ ((𝑥tpos 𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = ((𝑧𝐺𝑥)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) |
80 | | ovtpos 7367 |
. . . . 5
⊢ (𝑦tpos 𝐺𝑧) = (𝑧𝐺𝑦) |
81 | 80 | fveq1i 6192 |
. . . 4
⊢ ((𝑦tpos 𝐺𝑧)‘𝑔) = ((𝑧𝐺𝑦)‘𝑔) |
82 | 34 | fveq1i 6192 |
. . . 4
⊢ ((𝑥tpos 𝐺𝑦)‘𝑓) = ((𝑦𝐺𝑥)‘𝑓) |
83 | 81, 82 | oveq12i 6662 |
. . 3
⊢ (((𝑦tpos 𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑥tpos 𝐺𝑦)‘𝑓)) = (((𝑧𝐺𝑦)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑦𝐺𝑥)‘𝑓)) |
84 | 77, 79, 83 | 3eqtr4g 2681 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑥tpos 𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = (((𝑦tpos 𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑥tpos 𝐺𝑦)‘𝑓))) |
85 | 3, 6, 7, 8, 9, 10,
11, 12, 20, 23, 24, 27, 40, 57, 84 | isfuncd 16525 |
1
⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)tpos 𝐺) |