Metamath Proof Explorer

Theorem prstcprs

Description: The category is a preordered set. (Contributed by Zhi Wang, 20-Sep-2024)

Ref Expression
Hypotheses prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
Assertion prstcprs ⊢ φ → C ∈ Proset

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 eqidd ⊢ φ → Base K = Base K
4 1 2 3 prstcbas ⊢ φ → Base K = Base C
5 eqidd ⊢ φ → ≤ K = ≤ K
6 1 2 5 prstcleval ⊢ φ → ≤ K = ≤ C
7 fvex ⊢ ProsetToCat ⁡ K ∈ V
8 1 7 eqeltrdi ⊢ φ → C ∈ V
9 4 6 8 isprsd ⊢ φ → C ∈ Proset ↔ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x ≤ K x ∧ x ≤ K y ∧ y ≤ K z → x ≤ K z
10 3 5 2 isprsd ⊢ φ → K ∈ Proset ↔ ∀ x ∈ Base K ∀ y ∈ Base K ∀ z ∈ Base K x ≤ K x ∧ x ≤ K y ∧ y ≤ K z → x ≤ K z
11 9 10 bitr4d ⊢ φ → C ∈ Proset ↔ K ∈ Proset
12 2 11 mpbird ⊢ φ → C ∈ Proset