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	|- ( ph -> C = ( ProsetToCat ` K ) )
	postc.k	|- ( ph -> K e. Proset )
Assertion	postcpos	|- ( ph -> ( K e. Poset <-> C e. Poset ) )

Proof

Step	Hyp	Ref	Expression
1		postc.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		postc.k	|- ( ph -> K e. Proset )
3	1 2	prstcprs	|- ( ph -> C e. Proset )
4		eqidd	|- ( ph -> ( Base ` K ) = ( Base ` K ) )
5	1 2 4	prstcbas	|- ( ph -> ( Base ` K ) = ( Base ` C ) )
6		eqidd	|- ( ph -> ( le ` K ) = ( le ` K ) )
7	1 2 6	prstcle	|- ( ph -> ( x ( le ` K ) y <-> x ( le ` C ) y ) )
8	7	adantr	|- ( ( ph /\ ( x e. ( Base ` K ) /\ y e. ( Base ` K ) ) ) -> ( x ( le ` K ) y <-> x ( le ` C ) y ) )
9	2 3 4 5 8	pospropd	|- ( ph -> ( K e. Poset <-> C e. Poset ) )