Proof of Theorem oppcsect
Step | Hyp | Ref
| Expression |
1 | | oppcsect.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝐶) |
2 | | eqid 2738 |
. . . . . 6
⊢
(comp‘𝐶) =
(comp‘𝐶) |
3 | | oppcsect.o |
. . . . . 6
⊢ 𝑂 = (oppCat‘𝐶) |
4 | | oppcsect.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → 𝑋 ∈ 𝐵) |
6 | | oppcsect.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → 𝑌 ∈ 𝐵) |
8 | 1, 2, 3, 5, 7, 5 | oppcco 17427 |
. . . . 5
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺)) |
9 | | oppcsect.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ Cat) |
10 | 9 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → 𝐶 ∈ Cat) |
11 | | eqid 2738 |
. . . . . . . 8
⊢
(Id‘𝐶) =
(Id‘𝐶) |
12 | 3, 11 | oppcid 17432 |
. . . . . . 7
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) |
13 | 10, 12 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → (Id‘𝑂) = (Id‘𝐶)) |
14 | 13 | fveq1d 6776 |
. . . . 5
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → ((Id‘𝑂)‘𝑋) = ((Id‘𝐶)‘𝑋)) |
15 | 8, 14 | eqeq12d 2754 |
. . . 4
⊢ ((𝜑 ∧ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) → ((𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋) ↔ (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺) = ((Id‘𝐶)‘𝑋))) |
16 | 15 | pm5.32da 579 |
. . 3
⊢ (𝜑 → (((𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋)) ↔ ((𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺) = ((Id‘𝐶)‘𝑋)))) |
17 | | df-3an 1088 |
. . . 4
⊢ ((𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋)) ↔ ((𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋))) |
18 | | eqid 2738 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
19 | 18, 3 | oppchom 17425 |
. . . . . . 7
⊢ (𝑋(Hom ‘𝑂)𝑌) = (𝑌(Hom ‘𝐶)𝑋) |
20 | 19 | eleq2i 2830 |
. . . . . 6
⊢ (𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ↔ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) |
21 | 18, 3 | oppchom 17425 |
. . . . . . 7
⊢ (𝑌(Hom ‘𝑂)𝑋) = (𝑋(Hom ‘𝐶)𝑌) |
22 | 21 | eleq2i 2830 |
. . . . . 6
⊢ (𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋) ↔ 𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
23 | 20, 22 | anbi12ci 628 |
. . . . 5
⊢ ((𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋)) ↔ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋))) |
24 | 23 | anbi1i 624 |
. . . 4
⊢ (((𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋)) ↔ ((𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋))) |
25 | 17, 24 | bitri 274 |
. . 3
⊢ ((𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋)) ↔ ((𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋))) |
26 | | df-3an 1088 |
. . 3
⊢ ((𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺) = ((Id‘𝐶)‘𝑋)) ↔ ((𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋)) ∧ (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺) = ((Id‘𝐶)‘𝑋))) |
27 | 16, 25, 26 | 3bitr4g 314 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋)) ↔ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺) = ((Id‘𝐶)‘𝑋)))) |
28 | 3, 1 | oppcbas 17428 |
. . 3
⊢ 𝐵 = (Base‘𝑂) |
29 | | eqid 2738 |
. . 3
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
30 | | eqid 2738 |
. . 3
⊢
(comp‘𝑂) =
(comp‘𝑂) |
31 | | eqid 2738 |
. . 3
⊢
(Id‘𝑂) =
(Id‘𝑂) |
32 | | oppcsect.t |
. . 3
⊢ 𝑇 = (Sect‘𝑂) |
33 | 3 | oppccat 17433 |
. . . 4
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) |
34 | 9, 33 | syl 17 |
. . 3
⊢ (𝜑 → 𝑂 ∈ Cat) |
35 | 28, 29, 30, 31, 32, 34, 4, 6 | issect 17465 |
. 2
⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ (𝐹 ∈ (𝑋(Hom ‘𝑂)𝑌) ∧ 𝐺 ∈ (𝑌(Hom ‘𝑂)𝑋) ∧ (𝐺(〈𝑋, 𝑌〉(comp‘𝑂)𝑋)𝐹) = ((Id‘𝑂)‘𝑋)))) |
36 | | oppcsect.s |
. . 3
⊢ 𝑆 = (Sect‘𝐶) |
37 | 1, 18, 2, 11, 36, 9, 4, 6 | issect 17465 |
. 2
⊢ (𝜑 → (𝐺(𝑋𝑆𝑌)𝐹 ↔ (𝐺 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ 𝐹 ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (𝐹(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐺) = ((Id‘𝐶)‘𝑋)))) |
38 | 27, 35, 37 | 3bitr4d 311 |
1
⊢ (𝜑 → (𝐹(𝑋𝑇𝑌)𝐺 ↔ 𝐺(𝑋𝑆𝑌)𝐹)) |