This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
Assertion prstcthin ( 𝜑 → 𝐶 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
4 eqidd ⊢ ( 𝜑 → ( le ‘ 𝐶 ) = ( le ‘ 𝐶 ) )
5 1 2 4 prstchomval ⊢ ( 𝜑 → ( ( le ‘ 𝐶 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
6 ovex ⊢ ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ∈ V
7 0ex ⊢ ∅ ∈ V
8 ccoid ⊢ comp = Slot ( comp ‘ ndx )
9 8 setsid ⊢ ( ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) ∈ V ∧ ∅ ∈ V ) → ∅ = ( comp ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) ) )
10 6 7 9 mp2an ⊢ ∅ = ( comp ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
11 1 2 prstcval ⊢ ( 𝜑 → 𝐶 = ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
12 11 fveq2d ⊢ ( 𝜑 → ( comp ‘ 𝐶 ) = ( comp ‘ ( ( 𝐾 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝐾 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) ) )
13 10 12 eqtr4id ⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
14 1 2 prstcprs ⊢ ( 𝜑 → 𝐶 ∈ Proset )
15 3 5 13 4 14 prsthinc ⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ∅ ) ) )
16 15 simpld ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )