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 )