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 ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
Assertion prstcthin ⊢ φ → C ∈ ThinCat

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 eqidd ⊢ φ → Base C = Base C
4 eqidd ⊢ φ → ≤ C = ≤ C
5 1 2 4 prstchomval ⊢ φ → ≤ C × 1 𝑜 = Hom ⁡ C
6 ovex ⊢ K sSet Hom ⁡ ndx ≤ K × 1 𝑜 ∈ V
7 0ex ⊢ ∅ ∈ V
8 ccoid ⊢ comp = Slot comp ⁡ ndx
9 8 setsid ⊢ K sSet Hom ⁡ ndx ≤ K × 1 𝑜 ∈ V ∧ ∅ ∈ V → ∅ = comp ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
10 6 7 9 mp2an ⊢ ∅ = comp ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
11 1 2 prstcval ⊢ φ → C = K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
12 11 fveq2d ⊢ φ → comp ⁡ C = comp ⁡ K sSet Hom ⁡ ndx ≤ K × 1 𝑜 sSet comp ⁡ ndx ∅
13 10 12 eqtr4id ⊢ φ → ∅ = comp ⁡ C
14 1 2 prstcprs ⊢ φ → C ∈ Proset
15 3 5 13 4 14 prsthinc ⊢ φ → C ∈ ThinCat ∧ Id ⁡ C = y ∈ Base C ⟼ ∅
16 15 simpld ⊢ φ → C ∈ ThinCat