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

Metamath Proof Explorer

Theorem prstcprs

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

Ref Expression
Hypotheses prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
Assertion prstcprs ( 𝜑 → 𝐶 ∈ Proset )

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 prstcnid.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
4 1 2 3 prstcbas ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐶 ) )
5 eqidd ⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) )
6 1 2 5 prstcleval ⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐶 ) )
7 fvex ⊢ ( ProsetToCat ‘ 𝐾 ) ∈ V
8 1 7 eqeltrdi ⊢ ( 𝜑 → 𝐶 ∈ V )
9 4 6 8 isprsd ⊢ ( 𝜑 → ( 𝐶 ∈ Proset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
10 3 5 2 isprsd ⊢ ( 𝜑 → ( 𝐾 ∈ Proset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
11 9 10 bitr4d ⊢ ( 𝜑 → ( 𝐶 ∈ Proset ↔ 𝐾 ∈ Proset ) )
12 2 11 mpbird ⊢ ( 𝜑 → 𝐶 ∈ Proset )