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