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 )