Metamath Proof Explorer


Theorem prstcthin

Description: The preordered set is equipped with a thin category. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
prstcnid.k φKProset
Assertion prstcthin Could not format assertion : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-

Proof

Step Hyp Ref Expression
1 prstcnid.c Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2 prstcnid.k φKProset
3 eqidd φBaseC=BaseC
4 eqidd φC=C
5 1 2 4 prstchomval φC×1𝑜=HomC
6 ovex KsSetHomndxK×1𝑜V
7 0ex V
8 ccoid comp=Slotcompndx
9 8 setsid KsSetHomndxK×1𝑜VV=compKsSetHomndxK×1𝑜sSetcompndx
10 6 7 9 mp2an =compKsSetHomndxK×1𝑜sSetcompndx
11 1 2 prstcval φC=KsSetHomndxK×1𝑜sSetcompndx
12 11 fveq2d φcompC=compKsSetHomndxK×1𝑜sSetcompndx
13 10 12 eqtr4id φ=compC
14 1 2 prstcprs φCProset
15 3 5 13 4 14 prsthinc Could not format ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> (/) ) ) ) : No typesetting found for |- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. ( Base ` C ) |-> (/) ) ) ) with typecode |-
16 15 simpld Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-