postcposALT

Description: Alternate proof for postcpos . (Contributed by Zhi Wang, 25-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	postc.c	No typesetting found for \|- ( ph -> C = ( ProsetToCat ` K ) ) with typecode \|-
	postc.k	$⊢ φ \to K \in Proset$
Assertion	postcposALT	$⊢ φ \to (K \in Poset \leftrightarrow C \in Poset)$

Proof

Step	Hyp	Ref	Expression
1		postc.c	Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for \|- ( ph -> C = ( ProsetToCat ` K ) ) with typecode \|-
2		postc.k	$⊢ φ \to K \in Proset$
3		eqidd	$⊢ φ \to {Base}_{K} = {Base}_{K}$
4	1 2 3	prstcbas	$⊢ φ \to {Base}_{K} = {Base}_{C}$
5		eqidd	$⊢ φ \to \leq_{K} = \leq_{K}$
6	1 2 5	prstcle	$⊢ φ \to (x \leq_{K} y \leftrightarrow x \leq_{C} y)$
7	1 2 5	prstcle	$⊢ φ \to (y \leq_{K} x \leftrightarrow y \leq_{C} x)$
8	6 7	anbi12d	$⊢ φ \to ((x \leq_{K} y \land y \leq_{K} x) \leftrightarrow (x \leq_{C} y \land y \leq_{C} x))$
9	8	imbi1d	$⊢ φ \to (((x \leq_{K} y \land y \leq_{K} x) \to x = y) \leftrightarrow ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
10	4 9	raleqbidvv	$⊢ φ \to (\forall y \in {Base}_{K} ((x \leq_{K} y \land y \leq_{K} x) \to x = y) \leftrightarrow \forall y \in {Base}_{C} ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
11	4 10	raleqbidvv	$⊢ φ \to (\forall x \in {Base}_{K} \forall y \in {Base}_{K} ((x \leq_{K} y \land y \leq_{K} x) \to x = y) \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13		eqid	$⊢ \leq_{K} = \leq_{K}$
14	12 13	ispos2	$⊢ K \in Poset \leftrightarrow (K \in Proset \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} ((x \leq_{K} y \land y \leq_{K} x) \to x = y))$
15	14	baib	$⊢ K \in Proset \to (K \in Poset \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} ((x \leq_{K} y \land y \leq_{K} x) \to x = y))$
16	2 15	syl	$⊢ φ \to (K \in Poset \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} ((x \leq_{K} y \land y \leq_{K} x) \to x = y))$
17	1 2	prstcprs	$⊢ φ \to C \in Proset$
18		eqid	$⊢ {Base}_{C} = {Base}_{C}$
19		eqid	$⊢ \leq_{C} = \leq_{C}$
20	18 19	ispos2	$⊢ C \in Poset \leftrightarrow (C \in Proset \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
21	20	baib	$⊢ C \in Proset \to (C \in Poset \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
22	17 21	syl	$⊢ φ \to (C \in Poset \leftrightarrow \forall x \in {Base}_{C} \forall y \in {Base}_{C} ((x \leq_{C} y \land y \leq_{C} x) \to x = y))$
23	11 16 22	3bitr4d	$⊢ φ \to (K \in Poset \leftrightarrow C \in Poset)$

Metamath Proof Explorer

Theorem postcposALT

Proof