Theorem postcpos

Description: The converted category is a poset iff the original proset is a poset. (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	postc.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	postc.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
Assertion	postcpos	⊢ ( 𝜑 → ( 𝐾 ∈ Poset ↔ 𝐶 ∈ Poset ) )

Proof

Step	Hyp	Ref	Expression
1		postc.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		postc.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3	1 2	prstcprs	⊢ ( 𝜑 → 𝐶 ∈ Proset )
4		eqidd	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
5	1 2 4	prstcbas	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐶 ) )
6		eqidd	⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ 𝐾 ) )
7	1 2 6	prstcle	⊢ ( 𝜑 → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
8	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ 𝐶 ) 𝑦 ) )
9	2 3 4 5 8	pospropd	⊢ ( 𝜑 → ( 𝐾 ∈ Poset ↔ 𝐶 ∈ Poset ) )