Theorem catprs2

Description: A category equipped with the induced preorder, where an object x is defined to be "less than or equal to" y iff there is a morphism from x to y , is a preordered set, or a proset. The category might not be thin. See catprsc and catprsc2 for constructions satisfying the hypothesis "catprs.1". See catprs for a more primitive version. See prsthinc for constructing a thin category from a proset. (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	catprs.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
	catprs.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	catprs.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
	catprs.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	catprs2.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
Assertion	catprs2	⊢ ( 𝜑 → 𝐶 ∈ Proset )

Proof

Step	Hyp	Ref	Expression
1		catprs.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 𝐻 𝑦 ) ≠ ∅ ) )
2		catprs.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
3		catprs.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
4		catprs.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		catprs2.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
6	1 2 3 4	catprs	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( 𝑤 ≤ 𝑤 ∧ ( ( 𝑤 ≤ 𝑣 ∧ 𝑣 ≤ 𝑢 ) → 𝑤 ≤ 𝑢 ) ) )
7	6	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( 𝑤 ≤ 𝑤 ∧ ( ( 𝑤 ≤ 𝑣 ∧ 𝑣 ≤ 𝑢 ) → 𝑤 ≤ 𝑢 ) ) )
8	2 5 4	isprsd	⊢ ( 𝜑 → ( 𝐶 ∈ Proset ↔ ∀ 𝑤 ∈ 𝐵 ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( 𝑤 ≤ 𝑤 ∧ ( ( 𝑤 ≤ 𝑣 ∧ 𝑣 ≤ 𝑢 ) → 𝑤 ≤ 𝑢 ) ) ) )
9	7 8	mpbird	⊢ ( 𝜑 → 𝐶 ∈ Proset )