Definition df-cv

Description: Define the covers relation (on the Hilbert lattice). Definition 3.2.18 of PtakPulmannova p. 68, whose notation we use. Ptak/Pulmannova's notation A is read " B covers A " or " A is covered by B " , and it means that B is larger than A and there is nothing in between. See cvbr and cvbr2 for membership relations. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	df-cv	|- . | ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccv	|-
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4		cch	|- CH
5	3 4	wcel	|- x e. CH
6	2	cv	|- y
7	6 4	wcel	|- y e. CH
8	5 7	wa	|- ( x e. CH /\ y e. CH )
9	3 6	wpss	|- x C. y
10		vz	|- z
11	10	cv	|- z
12	3 11	wpss	|- x C. z
13	11 6	wpss	|- z C. y
14	12 13	wa	|- ( x C. z /\ z C. y )
15	14 10 4	wrex	|- E. z e. CH ( x C. z /\ z C. y )
16	15	wn	|- -. E. z e. CH ( x C. z /\ z C. y )
17	9 16	wa	|- ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) )
18	8 17	wa	|- ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) )
19	18 1 2	copab	|- { <. x , y >. | ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) ) }
20	0 19	wceq	|- . | ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) ) }