df-covers

Description: Define the covers relation ("is covered by") for posets. " a is covered by b " means that a is strictly less than b and there is nothing in between. See cvrval for the relation form. (Contributed by NM, 18-Sep-2011)

		Ref	Expression
	Assertion	df-covers	$⊢ ⋖ = (p \in V ⟼ \{⟨a, b⟩ \| ((a \in {Base}_{p} \land b \in {Base}_{p}) \land a <_{p} b \land \neg \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvr	$class ⋖$
1		vp	$setvar p$
2		cvv	$class V$
3		va	$setvar a$
4		vb	$setvar b$
5	3	cv	$setvar a$
6		cbs	$class Base$
7	1	cv	$setvar p$
8	7 6	cfv	$class {Base}_{p}$
9	5 8	wcel	$wff a \in {Base}_{p}$
10	4	cv	$setvar b$
11	10 8	wcel	$wff b \in {Base}_{p}$
12	9 11	wa	$wff (a \in {Base}_{p} \land b \in {Base}_{p})$
13		cplt	$class lt$
14	7 13	cfv	$class <_{p}$
15	5 10 14	wbr	$wff a <_{p} b$
16		vz	$setvar z$
17	16	cv	$setvar z$
18	5 17 14	wbr	$wff a <_{p} z$
19	17 10 14	wbr	$wff z <_{p} b$
20	18 19	wa	$wff (a <_{p} z \land z <_{p} b)$
21	20 16 8	wrex	$wff \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b)$
22	21	wn	$wff \neg \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b)$
23	12 15 22	w3a	$wff ((a \in {Base}_{p} \land b \in {Base}_{p}) \land a <_{p} b \land \neg \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b))$
24	23 3 4	copab	$class \{⟨a, b⟩ \| ((a \in {Base}_{p} \land b \in {Base}_{p}) \land a <_{p} b \land \neg \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b))\}$
25	1 2 24	cmpt	$class (p \in V ⟼ \{⟨a, b⟩ \| ((a \in {Base}_{p} \land b \in {Base}_{p}) \land a <_{p} b \land \neg \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b))\})$
26	0 25	wceq	$wff ⋖ = (p \in V ⟼ \{⟨a, b⟩ \| ((a \in {Base}_{p} \land b \in {Base}_{p}) \land a <_{p} b \land \neg \exists z \in {Base}_{p} (a <_{p} z \land z <_{p} b))\})$

Metamath Proof Explorer

Definition df-covers

Detailed syntax breakdown