isposd

Description: Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014) (Revised by AV, 26-Apr-2024)

	Ref	Expression
Hypotheses	isposd.k	$⊢ φ \to K \in V$
	isposd.b	$⊢ φ \to B = {Base}_{K}$
	isposd.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{K}$
	isposd.1	$⊢ (φ \land x \in B) \to x \underset{˙}{\leq} x$
	isposd.2	$⊢ (φ \land x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
	isposd.3	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
Assertion	isposd	$⊢ φ \to K \in Poset$

Proof

Step	Hyp	Ref	Expression
1		isposd.k	$⊢ φ \to K \in V$
2		isposd.b	$⊢ φ \to B = {Base}_{K}$
3		isposd.l	$⊢ φ \to \underset{˙}{\leq} = \leq_{K}$
4		isposd.1	$⊢ (φ \land x \in B) \to x \underset{˙}{\leq} x$
5		isposd.2	$⊢ (φ \land x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
6		isposd.3	$⊢ (φ \land (x \in B \land y \in B \land z \in B)) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
7	1	elexd	$⊢ φ \to K \in V$
8	4	adantrr	$⊢ (φ \land (x \in B \land y \in B)) \to x \underset{˙}{\leq} x$
9	8	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land z \in B) \to x \underset{˙}{\leq} x$
10	5	3expb	$⊢ (φ \land (x \in B \land y \in B)) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
11	10	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land z \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
12	6	3exp2	$⊢ φ \to (x \in B \to (y \in B \to (z \in B \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))))$
13	12	imp42	$⊢ ((φ \land (x \in B \land y \in B)) \land z \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
14	9 11 13	3jca	$⊢ ((φ \land (x \in B \land y \in B)) \land z \in B) \to (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))$
15	14	ralrimiva	$⊢ (φ \land (x \in B \land y \in B)) \to \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))$
16	15	ralrimivva	$⊢ φ \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))$
17	3	breqd	$⊢ φ \to (x \underset{˙}{\leq} x \leftrightarrow x \leq_{K} x)$
18	3	breqd	$⊢ φ \to (x \underset{˙}{\leq} y \leftrightarrow x \leq_{K} y)$
19	3	breqd	$⊢ φ \to (y \underset{˙}{\leq} x \leftrightarrow y \leq_{K} x)$
20	18 19	anbi12d	$⊢ φ \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \leftrightarrow (x \leq_{K} y \land y \leq_{K} x))$
21	20	imbi1d	$⊢ φ \to (((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y) \leftrightarrow ((x \leq_{K} y \land y \leq_{K} x) \to x = y))$
22	3	breqd	$⊢ φ \to (y \underset{˙}{\leq} z \leftrightarrow y \leq_{K} z)$
23	18 22	anbi12d	$⊢ φ \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \leftrightarrow (x \leq_{K} y \land y \leq_{K} z))$
24	3	breqd	$⊢ φ \to (x \underset{˙}{\leq} z \leftrightarrow x \leq_{K} z)$
25	23 24	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))$
26	17 21 25	3anbi123d	$⊢ φ \to ((x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y) \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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
27	2 26	raleqbidv	$⊢ φ \to (\forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y) \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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
28	2 27	raleqbidv	$⊢ φ \to (\forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y) \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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
29	2 28	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} x) \to x = y) \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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
30	29	anbi2d	$⊢ φ \to ((K \in V \land \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))) \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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))))$
31	7 16 30	mpbi2and	$⊢ φ \to (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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33		eqid	$⊢ \leq_{K} = \leq_{K}$
34	32 33	ispos	$⊢ K \in Poset \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} x) \to x = y) \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
35	31 34	sylibr	$⊢ φ \to K \in Poset$

Metamath Proof Explorer

Theorem isposd

Proof