Metamath Proof Explorer

Definition 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 
|-  { <. 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccvr 
 |-
1 vp 
 |-  p
2 cvv 
 |-  _V
3 va 
 |-  a
4 vb 
 |-  b
5 3 cv 
 |-  a
6 cbs 
 |-  Base
7 1 cv 
 |-  p
8 7 6 cfv 
 |-  ( Base ` p )
9 5 8 wcel 
 |-  a e. ( Base ` p )
10 4 cv 
 |-  b
11 10 8 wcel 
 |-  b e. ( Base ` p )
12 9 11 wa 
 |-  ( a e. ( Base ` p ) /\ b e. ( Base ` p ) )
13 cplt 
 |-  lt
14 7 13 cfv 
 |-  ( lt ` p )
15 5 10 14 wbr 
 |-  a ( lt ` p ) b
16 vz 
 |-  z
17 16 cv 
 |-  z
18 5 17 14 wbr 
 |-  a ( lt ` p ) z
19 17 10 14 wbr 
 |-  z ( lt ` p ) b
20 18 19 wa 
 |-  ( a ( lt ` p ) z /\ z ( lt ` p ) b )
21 20 16 8 wrex 
 |-  E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b )
22 21 wn 
 |-  -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b )
23 12 15 22 w3a 
 |-  ( ( 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 ) )
24 23 3 4 copab 
 |-  { <. 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 ) ) }
25 1 2 24 cmpt 
 |-  ( 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 ) ) } )
26 0 25 wceq 
 |-   { <. 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 ) ) } )