isprsd

Description: Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	isprsd.b	$⊢ φ \to B = {Base}_{K}$
	isprsd.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{K}$
	isprsd.k	$⊢ φ \to K \in V$
Assertion	isprsd	$⊢ φ \to (K \in Proset \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$

Proof

Step	Hyp	Ref	Expression
1		isprsd.b	$⊢ φ \to B = {Base}_{K}$
2		isprsd.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{K}$
3		isprsd.k	$⊢ φ \to K \in V$
4	3	elexd	$⊢ φ \to K \in V$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6		eqid	$⊢ \leq_{K} = \leq_{K}$
7	5 6	isprs	$⊢ K \in Proset \leftrightarrow (K \in V \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
8	7	baib	$⊢ K \in V \to (K \in Proset \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
9	4 8	syl	$⊢ φ \to (K \in Proset \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
10	2	breqd	$⊢ φ \to (x \underset{˙}{\leq} x \leftrightarrow x \leq_{K} x)$
11	2	breqd	$⊢ φ \to (x \underset{˙}{\leq} y \leftrightarrow x \leq_{K} y)$
12	2	breqd	$⊢ φ \to (y \underset{˙}{\leq} z \leftrightarrow y \leq_{K} z)$
13	11 12	anbi12d	$⊢ φ \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \leftrightarrow (x \leq_{K} y \land y \leq_{K} z))$
14	2	breqd	$⊢ φ \to (x \underset{˙}{\leq} z \leftrightarrow x \leq_{K} z)$
15	13 14	imbi12d	$⊢ φ \to (((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z) \leftrightarrow ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
16	10 15	anbi12d	$⊢ φ \to ((x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)) \leftrightarrow (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
17	1 16	raleqbidv	$⊢ φ \to (\forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)) \leftrightarrow \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
18	1 17	raleqbidv	$⊢ φ \to (\forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)) \leftrightarrow \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
19	1 18	raleqbidv	$⊢ φ \to (\forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)) \leftrightarrow \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
20	9 19	bitr4d	$⊢ φ \to (K \in Proset \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$

Metamath Proof Explorer

Theorem isprsd

Proof