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

Metamath Proof Explorer

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 ⊢ φ → ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ x H y ≠ ∅
catprs.b ⊢ φ → B = Base C
catprs.h ⊢ φ → H = Hom ⁡ C
catprs.c ⊢ φ → C ∈ Cat
catprs2.l ⊢ φ → ≤ ˙ = ≤ C
Assertion catprs2 ⊢ φ → C ∈ Proset

Proof

Step Hyp Ref Expression
1 catprs.1 ⊢ φ → ∀ x ∈ B ∀ y ∈ B x ≤ ˙ y ↔ x H y ≠ ∅
2 catprs.b ⊢ φ → B = Base C
3 catprs.h ⊢ φ → H = Hom ⁡ C
4 catprs.c ⊢ φ → C ∈ Cat
5 catprs2.l ⊢ φ → ≤ ˙ = ≤ C
6 1 2 3 4 catprs ⊢ φ ∧ w ∈ B ∧ v ∈ B ∧ u ∈ B → w ≤ ˙ w ∧ w ≤ ˙ v ∧ v ≤ ˙ u → w ≤ ˙ u
7 6 ralrimivvva ⊢ φ → ∀ w ∈ B ∀ v ∈ B ∀ u ∈ B w ≤ ˙ w ∧ w ≤ ˙ v ∧ v ≤ ˙ u → w ≤ ˙ u
8 2 5 4 isprsd ⊢ φ → C ∈ Proset ↔ ∀ w ∈ B ∀ v ∈ B ∀ u ∈ B w ≤ ˙ w ∧ w ≤ ˙ v ∧ v ≤ ˙ u → w ≤ ˙ u
9 7 8 mpbird ⊢ φ → C ∈ Proset