Step | Hyp | Ref
| Expression |
1 | | eqid 2734 |
. 2
⊢
(CatCat‘𝑈) =
(CatCat‘𝑈) |
2 | | eqid 2734 |
. 2
⊢
(Base‘𝐷) =
(Base‘𝐷) |
3 | | eqid 2734 |
. 2
⊢
(Base‘𝑂) =
(Base‘𝑂) |
4 | | eqid 2734 |
. 2
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
5 | | eqid 2734 |
. 2
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) |
6 | | oduoppcciso.u |
. 2
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
7 | | oduoppcciso.d |
. 2
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
8 | | oduoppcciso.o |
. 2
⊢ (𝜑 → 𝑂 ∈ 𝑈) |
9 | | oduoppcbas.d |
. . 3
⊢ (𝜑 → 𝐷 = (ProsetToCat‘(ODual‘𝐾))) |
10 | | prstcnid.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Proset ) |
11 | | eqid 2734 |
. . . . 5
⊢
(ODual‘𝐾) =
(ODual‘𝐾) |
12 | 11 | oduprs 18357 |
. . . 4
⊢ (𝐾 ∈ Proset →
(ODual‘𝐾) ∈
Proset ) |
13 | 10, 12 | syl 17 |
. . 3
⊢ (𝜑 → (ODual‘𝐾) ∈ Proset
) |
14 | 9, 13 | prstcthin 48876 |
. 2
⊢ (𝜑 → 𝐷 ∈ ThinCat) |
15 | | prstcnid.c |
. . . 4
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) |
16 | 15, 10 | prstcthin 48876 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ThinCat) |
17 | | oduoppcbas.o |
. . . 4
⊢ 𝑂 = (oppCat‘𝐶) |
18 | 17 | oppcthin 48838 |
. . 3
⊢ (𝐶 ∈ ThinCat → 𝑂 ∈
ThinCat) |
19 | 16, 18 | syl 17 |
. 2
⊢ (𝜑 → 𝑂 ∈ ThinCat) |
20 | | f1oi 6886 |
. . 3
⊢ ( I
↾ (Base‘𝐷)):(Base‘𝐷)–1-1-onto→(Base‘𝐷) |
21 | 15, 10, 9, 17 | oduoppcbas 48880 |
. . . 4
⊢ (𝜑 → (Base‘𝐷) = (Base‘𝑂)) |
22 | 21 | f1oeq3d 6845 |
. . 3
⊢ (𝜑 → (( I ↾
(Base‘𝐷)):(Base‘𝐷)–1-1-onto→(Base‘𝐷) ↔ ( I ↾ (Base‘𝐷)):(Base‘𝐷)–1-1-onto→(Base‘𝑂))) |
23 | 20, 22 | mpbii 233 |
. 2
⊢ (𝜑 → ( I ↾
(Base‘𝐷)):(Base‘𝐷)–1-1-onto→(Base‘𝑂)) |
24 | | eqid 2734 |
. . . . . . 7
⊢
(le‘𝐾) =
(le‘𝐾) |
25 | | eqid 2734 |
. . . . . . 7
⊢
(le‘(ODual‘𝐾)) = (le‘(ODual‘𝐾)) |
26 | 11, 24, 25 | oduleg 18346 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷)) → (𝑥(le‘(ODual‘𝐾))𝑦 ↔ 𝑦(le‘𝐾)𝑥)) |
27 | 26 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(le‘(ODual‘𝐾))𝑦 ↔ 𝑦(le‘𝐾)𝑥)) |
28 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐷 = (ProsetToCat‘(ODual‘𝐾))) |
29 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐾 ∈ Proset ) |
30 | 29, 12 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (ODual‘𝐾) ∈ Proset ) |
31 | | eqidd 2735 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘(ODual‘𝐾)) =
(le‘(ODual‘𝐾))) |
32 | 28, 30, 31 | prstcleval 48868 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘(ODual‘𝐾)) = (le‘𝐷)) |
33 | | eqidd 2735 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Hom ‘𝐷) = (Hom ‘𝐷)) |
34 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐷)) |
35 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐷)) |
36 | 28, 30, 32, 33, 34, 35 | prstchom 48877 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(le‘(ODual‘𝐾))𝑦 ↔ (𝑥(Hom ‘𝐷)𝑦) ≠ ∅)) |
37 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐶 = (ProsetToCat‘𝐾)) |
38 | | eqidd 2735 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘𝐾) = (le‘𝐾)) |
39 | 37, 29, 38 | prstcleval 48868 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘𝐾) = (le‘𝐶)) |
40 | | eqidd 2735 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Hom ‘𝐶) = (Hom ‘𝐶)) |
41 | | eqid 2734 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
42 | 17, 41 | oppcbas 17763 |
. . . . . . . . 9
⊢
(Base‘𝐶) =
(Base‘𝑂) |
43 | 21, 42 | eqtr4di 2792 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐷) = (Base‘𝐶)) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Base‘𝐷) = (Base‘𝐶)) |
45 | 35, 44 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐶)) |
46 | 34, 44 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐶)) |
47 | 37, 29, 39, 40, 45, 46 | prstchom 48877 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑦(le‘𝐾)𝑥 ↔ (𝑦(Hom ‘𝐶)𝑥) ≠ ∅)) |
48 | 27, 36, 47 | 3bitr3d 309 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(Hom ‘𝐷)𝑦) ≠ ∅ ↔ (𝑦(Hom ‘𝐶)𝑥) ≠ ∅)) |
49 | 48 | necon4bid 2983 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(Hom ‘𝐷)𝑦) = ∅ ↔ (𝑦(Hom ‘𝐶)𝑥) = ∅)) |
50 | | fvresi 7192 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝐷) → (( I ↾
(Base‘𝐷))‘𝑥) = 𝑥) |
51 | 50 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (( I ↾ (Base‘𝐷))‘𝑥) = 𝑥) |
52 | | fvresi 7192 |
. . . . . . 7
⊢ (𝑦 ∈ (Base‘𝐷) → (( I ↾
(Base‘𝐷))‘𝑦) = 𝑦) |
53 | 52 | ad2antll 729 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (( I ↾ (Base‘𝐷))‘𝑦) = 𝑦) |
54 | 51, 53 | oveq12d 7448 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((( I ↾ (Base‘𝐷))‘𝑥)(Hom ‘𝑂)(( I ↾ (Base‘𝐷))‘𝑦)) = (𝑥(Hom ‘𝑂)𝑦)) |
55 | | eqid 2734 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
56 | 55, 17 | oppchom 17760 |
. . . . 5
⊢ (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥) |
57 | 54, 56 | eqtrdi 2790 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((( I ↾ (Base‘𝐷))‘𝑥)(Hom ‘𝑂)(( I ↾ (Base‘𝐷))‘𝑦)) = (𝑦(Hom ‘𝐶)𝑥)) |
58 | 57 | eqeq1d 2736 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (((( I ↾ (Base‘𝐷))‘𝑥)(Hom ‘𝑂)(( I ↾ (Base‘𝐷))‘𝑦)) = ∅ ↔ (𝑦(Hom ‘𝐶)𝑥) = ∅)) |
59 | 49, 58 | bitr4d 282 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(Hom ‘𝐷)𝑦) = ∅ ↔ ((( I ↾
(Base‘𝐷))‘𝑥)(Hom ‘𝑂)(( I ↾ (Base‘𝐷))‘𝑦)) = ∅)) |
60 | 1, 2, 3, 4, 5, 6, 7, 8, 14, 19, 23, 59 | thinccisod 48849 |
1
⊢ (𝜑 → 𝐷( ≃𝑐
‘(CatCat‘𝑈))𝑂) |