| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2736 |
. 2
⊢
(CatCat‘𝑈) =
(CatCat‘𝑈) |
| 2 | | eqid 2736 |
. 2
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 3 | | eqid 2736 |
. 2
⊢
(Base‘𝑂) =
(Base‘𝑂) |
| 4 | | eqid 2736 |
. 2
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 5 | | eqid 2736 |
. 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 2736 |
. . . . 5
⊢
(ODual‘𝐾) =
(ODual‘𝐾) |
| 12 | 11 | oduprs 18342 |
. . . 4
⊢ (𝐾 ∈ Proset →
(ODual‘𝐾) ∈
Proset ) |
| 13 | 10, 12 | syl 17 |
. . 3
⊢ (𝜑 → (ODual‘𝐾) ∈ Proset
) |
| 14 | 9, 13 | prstcthin 49141 |
. 2
⊢ (𝜑 → 𝐷 ∈ ThinCat) |
| 15 | | prstcnid.c |
. . . 4
⊢ (𝜑 → 𝐶 = (ProsetToCat‘𝐾)) |
| 16 | 15, 10 | prstcthin 49141 |
. . 3
⊢ (𝜑 → 𝐶 ∈ ThinCat) |
| 17 | | oduoppcbas.o |
. . . 4
⊢ 𝑂 = (oppCat‘𝐶) |
| 18 | 17 | oppcthin 49063 |
. . 3
⊢ (𝐶 ∈ ThinCat → 𝑂 ∈
ThinCat) |
| 19 | 16, 18 | syl 17 |
. 2
⊢ (𝜑 → 𝑂 ∈ ThinCat) |
| 20 | | f1oi 6884 |
. . 3
⊢ ( I
↾ (Base‘𝐷)):(Base‘𝐷)–1-1-onto→(Base‘𝐷) |
| 21 | 15, 10, 9, 17 | oduoppcbas 49145 |
. . . 4
⊢ (𝜑 → (Base‘𝐷) = (Base‘𝑂)) |
| 22 | 21 | f1oeq3d 6843 |
. . 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 2736 |
. . . . . . 7
⊢
(le‘𝐾) =
(le‘𝐾) |
| 25 | | eqid 2736 |
. . . . . . 7
⊢
(le‘(ODual‘𝐾)) = (le‘(ODual‘𝐾)) |
| 26 | 11, 24, 25 | oduleg 18331 |
. . . . . 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 2737 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘(ODual‘𝐾)) =
(le‘(ODual‘𝐾))) |
| 32 | 28, 30, 31 | prstcleval 49133 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘(ODual‘𝐾)) = (le‘𝐷)) |
| 33 | | eqidd 2737 |
. . . . . 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 49142 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(le‘(ODual‘𝐾))𝑦 ↔ (𝑥(Hom ‘𝐷)𝑦) ≠ ∅)) |
| 37 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐶 = (ProsetToCat‘𝐾)) |
| 38 | | eqidd 2737 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘𝐾) = (le‘𝐾)) |
| 39 | 37, 29, 38 | prstcleval 49133 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (le‘𝐾) = (le‘𝐶)) |
| 40 | | eqidd 2737 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Hom ‘𝐶) = (Hom ‘𝐶)) |
| 41 | | eqid 2736 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 42 | 17, 41 | oppcbas 17757 |
. . . . . . . . 9
⊢
(Base‘𝐶) =
(Base‘𝑂) |
| 43 | 21, 42 | eqtr4di 2794 |
. . . . . . . 8
⊢ (𝜑 → (Base‘𝐷) = (Base‘𝐶)) |
| 44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Base‘𝐷) = (Base‘𝐶)) |
| 45 | 35, 44 | eleqtrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐶)) |
| 46 | 34, 44 | eleqtrd 2842 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐶)) |
| 47 | 37, 29, 39, 40, 45, 46 | prstchom 49142 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑦(le‘𝐾)𝑥 ↔ (𝑦(Hom ‘𝐶)𝑥) ≠ ∅)) |
| 48 | 27, 36, 47 | 3bitr3d 309 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(Hom ‘𝐷)𝑦) ≠ ∅ ↔ (𝑦(Hom ‘𝐶)𝑥) ≠ ∅)) |
| 49 | 48 | necon4bid 2985 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(Hom ‘𝐷)𝑦) = ∅ ↔ (𝑦(Hom ‘𝐶)𝑥) = ∅)) |
| 50 | | fvresi 7191 |
. . . . . . 7
⊢ (𝑥 ∈ (Base‘𝐷) → (( I ↾
(Base‘𝐷))‘𝑥) = 𝑥) |
| 51 | 50 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (( I ↾ (Base‘𝐷))‘𝑥) = 𝑥) |
| 52 | | fvresi 7191 |
. . . . . . 7
⊢ (𝑦 ∈ (Base‘𝐷) → (( I ↾
(Base‘𝐷))‘𝑦) = 𝑦) |
| 53 | 52 | ad2antll 729 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (( I ↾ (Base‘𝐷))‘𝑦) = 𝑦) |
| 54 | 51, 53 | oveq12d 7447 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((( I ↾ (Base‘𝐷))‘𝑥)(Hom ‘𝑂)(( I ↾ (Base‘𝐷))‘𝑦)) = (𝑥(Hom ‘𝑂)𝑦)) |
| 55 | | eqid 2736 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 56 | 55, 17 | oppchom 17754 |
. . . . 5
⊢ (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥) |
| 57 | 54, 56 | eqtrdi 2792 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((( I ↾ (Base‘𝐷))‘𝑥)(Hom ‘𝑂)(( I ↾ (Base‘𝐷))‘𝑦)) = (𝑦(Hom ‘𝐶)𝑥)) |
| 58 | 57 | eqeq1d 2738 |
. . 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 49079 |
1
⊢ (𝜑 → 𝐷( ≃𝑐
‘(CatCat‘𝑈))𝑂) |