Definition df-covers 34553

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 34556 for the relation form. (Contributed by NM, 18-Sep-2011.)

Assertion

Ref	Expression
df-covers	|- <o = ( p e. _V |-> { <. a , b >. | ( ( a e. ( Base ` p ) /\ b e. ( Base ` p ) ) /\ a ( lt ` p ) b /\ -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b ) ) } )

Distinct variable group:   z, p, a, b

Detailed syntax breakdown of Definition df-covers

Step	Hyp	Ref	Expression
1		ccvr 34549	. 2 class <o
2		vp	. . 3 setvar p
3		cvv 3200	. . 3 class _V
4		va	. . . . . . . 8 setvar a
5	4	cv 1482	. . . . . . 7 class a
6	2	cv 1482	. . . . . . . 8 class p
7		cbs 15857	. . . . . . . 8 class Base
8	6, 7	cfv 5888	. . . . . . 7 class ( Base ` p )
9	5, 8	wcel 1990	. . . . . 6 wff a e. ( Base ` p )
10		vb	. . . . . . . 8 setvar b
11	10	cv 1482	. . . . . . 7 class b
12	11, 8	wcel 1990	. . . . . 6 wff b e. ( Base ` p )
13	9, 12	wa 384	. . . . 5 wff ( a e. ( Base ` p ) /\ b e. ( Base ` p ) )
14		cplt 16941	. . . . . . 7 class lt
15	6, 14	cfv 5888	. . . . . 6 class ( lt ` p )
16	5, 11, 15	wbr 4653	. . . . 5 wff a ( lt ` p ) b
17		vz	. . . . . . . . . 10 setvar z
18	17	cv 1482	. . . . . . . . 9 class z
19	5, 18, 15	wbr 4653	. . . . . . . 8 wff a ( lt ` p ) z
20	18, 11, 15	wbr 4653	. . . . . . . 8 wff z ( lt ` p ) b
21	19, 20	wa 384	. . . . . . 7 wff ( a ( lt ` p ) z /\ z ( lt ` p ) b )
22	21, 17, 8	wrex 2913	. . . . . 6 wff E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b )
23	22	wn 3	. . . . 5 wff -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b )
24	13, 16, 23	w3a 1037	. . . 4 wff ( ( a e. ( Base ` p ) /\ b e. ( Base ` p ) ) /\ a ( lt ` p ) b /\ -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b ) )
25	24, 4, 10	copab 4712	. . 3 class { <. a , b >. | ( ( a e. ( Base ` p ) /\ b e. ( Base ` p ) ) /\ a ( lt ` p ) b /\ -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b ) ) }
26	2, 3, 25	cmpt 4729	. 2 class ( p e. _V |-> { <. a , b >. | ( ( a e. ( Base ` p ) /\ b e. ( Base ` p ) ) /\ a ( lt ` p ) b /\ -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b ) ) } )
27	1, 26	wceq 1483	1 wff <o = ( p e. _V |-> { <. a , b >. | ( ( a e. ( Base ` p ) /\ b e. ( Base ` p ) ) /\ a ( lt ` p ) b /\ -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b ) ) } )

This definition is referenced by:  cvrfval  34555