| Step |
Hyp |
Ref |
Expression |
| 1 |
|
prstcnid.c |
|- ( ph -> C = ( ProsetToCat ` K ) ) |
| 2 |
|
prstcnid.k |
|- ( ph -> K e. Proset ) |
| 3 |
|
oduoppcbas.d |
|- ( ph -> D = ( ProsetToCat ` ( ODual ` K ) ) ) |
| 4 |
|
oduoppcbas.o |
|- O = ( oppCat ` C ) |
| 5 |
|
oduoppcciso.u |
|- ( ph -> U e. V ) |
| 6 |
|
oduoppcciso.d |
|- ( ph -> D e. U ) |
| 7 |
|
oduoppcciso.o |
|- ( ph -> O e. U ) |
| 8 |
|
eqid |
|- ( CatCat ` U ) = ( CatCat ` U ) |
| 9 |
|
eqid |
|- ( Base ` D ) = ( Base ` D ) |
| 10 |
|
eqid |
|- ( Base ` O ) = ( Base ` O ) |
| 11 |
|
eqid |
|- ( Hom ` D ) = ( Hom ` D ) |
| 12 |
|
eqid |
|- ( Hom ` O ) = ( Hom ` O ) |
| 13 |
|
eqid |
|- ( ODual ` K ) = ( ODual ` K ) |
| 14 |
13
|
oduprs |
|- ( K e. Proset -> ( ODual ` K ) e. Proset ) |
| 15 |
2 14
|
syl |
|- ( ph -> ( ODual ` K ) e. Proset ) |
| 16 |
3 15
|
prstcthin |
|- ( ph -> D e. ThinCat ) |
| 17 |
1 2
|
prstcthin |
|- ( ph -> C e. ThinCat ) |
| 18 |
4
|
oppcthin |
|- ( C e. ThinCat -> O e. ThinCat ) |
| 19 |
17 18
|
syl |
|- ( ph -> O e. ThinCat ) |
| 20 |
|
f1oi |
|- ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) |
| 21 |
1 2 3 4
|
oduoppcbas |
|- ( ph -> ( Base ` D ) = ( Base ` O ) ) |
| 22 |
21
|
f1oeq3d |
|- ( ph -> ( ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` D ) <-> ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` O ) ) ) |
| 23 |
20 22
|
mpbii |
|- ( ph -> ( _I |` ( Base ` D ) ) : ( Base ` D ) -1-1-onto-> ( Base ` O ) ) |
| 24 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
| 25 |
|
eqid |
|- ( le ` ( ODual ` K ) ) = ( le ` ( ODual ` K ) ) |
| 26 |
13 24 25
|
oduleg |
|- ( ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) -> ( x ( le ` ( ODual ` K ) ) y <-> y ( le ` K ) x ) ) |
| 27 |
26
|
adantl |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( le ` ( ODual ` K ) ) y <-> y ( le ` K ) x ) ) |
| 28 |
3
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> D = ( ProsetToCat ` ( ODual ` K ) ) ) |
| 29 |
2
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> K e. Proset ) |
| 30 |
29 14
|
syl |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ODual ` K ) e. Proset ) |
| 31 |
|
eqidd |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` ( ODual ` K ) ) = ( le ` ( ODual ` K ) ) ) |
| 32 |
28 30 31
|
prstcleval |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` ( ODual ` K ) ) = ( le ` D ) ) |
| 33 |
|
eqidd |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Hom ` D ) = ( Hom ` D ) ) |
| 34 |
|
simprl |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` D ) ) |
| 35 |
|
simprr |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` D ) ) |
| 36 |
28 30 32 33 34 35
|
prstchom |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( x ( le ` ( ODual ` K ) ) y <-> ( x ( Hom ` D ) y ) =/= (/) ) ) |
| 37 |
1
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> C = ( ProsetToCat ` K ) ) |
| 38 |
|
eqidd |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` K ) = ( le ` K ) ) |
| 39 |
37 29 38
|
prstcleval |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( le ` K ) = ( le ` C ) ) |
| 40 |
|
eqidd |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Hom ` C ) = ( Hom ` C ) ) |
| 41 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
| 42 |
4 41
|
oppcbas |
|- ( Base ` C ) = ( Base ` O ) |
| 43 |
21 42
|
eqtr4di |
|- ( ph -> ( Base ` D ) = ( Base ` C ) ) |
| 44 |
43
|
adantr |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( Base ` D ) = ( Base ` C ) ) |
| 45 |
35 44
|
eleqtrd |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> y e. ( Base ` C ) ) |
| 46 |
34 44
|
eleqtrd |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> x e. ( Base ` C ) ) |
| 47 |
37 29 39 40 45 46
|
prstchom |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( y ( le ` K ) x <-> ( y ( Hom ` C ) x ) =/= (/) ) ) |
| 48 |
27 36 47
|
3bitr3d |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x ( Hom ` D ) y ) =/= (/) <-> ( y ( Hom ` C ) x ) =/= (/) ) ) |
| 49 |
48
|
necon4bid |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x ( Hom ` D ) y ) = (/) <-> ( y ( Hom ` C ) x ) = (/) ) ) |
| 50 |
|
fvresi |
|- ( x e. ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) ` x ) = x ) |
| 51 |
50
|
ad2antrl |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( _I |` ( Base ` D ) ) ` x ) = x ) |
| 52 |
|
fvresi |
|- ( y e. ( Base ` D ) -> ( ( _I |` ( Base ` D ) ) ` y ) = y ) |
| 53 |
52
|
ad2antll |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( _I |` ( Base ` D ) ) ` y ) = y ) |
| 54 |
51 53
|
oveq12d |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( ( _I |` ( Base ` D ) ) ` x ) ( Hom ` O ) ( ( _I |` ( Base ` D ) ) ` y ) ) = ( x ( Hom ` O ) y ) ) |
| 55 |
|
eqid |
|- ( Hom ` C ) = ( Hom ` C ) |
| 56 |
55 4
|
oppchom |
|- ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x ) |
| 57 |
54 56
|
eqtrdi |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( ( _I |` ( Base ` D ) ) ` x ) ( Hom ` O ) ( ( _I |` ( Base ` D ) ) ` y ) ) = ( y ( Hom ` C ) x ) ) |
| 58 |
57
|
eqeq1d |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( ( ( _I |` ( Base ` D ) ) ` x ) ( Hom ` O ) ( ( _I |` ( Base ` D ) ) ` y ) ) = (/) <-> ( y ( Hom ` C ) x ) = (/) ) ) |
| 59 |
49 58
|
bitr4d |
|- ( ( ph /\ ( x e. ( Base ` D ) /\ y e. ( Base ` D ) ) ) -> ( ( x ( Hom ` D ) y ) = (/) <-> ( ( ( _I |` ( Base ` D ) ) ` x ) ( Hom ` O ) ( ( _I |` ( Base ` D ) ) ` y ) ) = (/) ) ) |
| 60 |
8 9 10 11 12 5 6 7 16 19 23 59
|
thinccisod |
|- ( ph -> D ( ~=c ` ( CatCat ` U ) ) O ) |