Definition df-cv 29138

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 <oH B 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 29141 and cvbr2 29142 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)

Assertion

Ref	Expression
df-cv	|- <oH = { <. x , y >. | ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) ) }

Distinct variable group:   x, y, z

Detailed syntax breakdown of Definition df-cv

Step	Hyp	Ref	Expression
1		ccv 27821	. 2 class <oH
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		cch 27786	. . . . . 6 class CH
5	3, 4	wcel 1990	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8	7, 4	wcel 1990	. . . . 5 wff y e. CH
9	5, 8	wa 384	. . . 4 wff ( x e. CH /\ y e. CH )
10	3, 7	wpss 3575	. . . . 5 wff x C. y
11		vz	. . . . . . . . . 10 setvar z
12	11	cv 1482	. . . . . . . . 9 class z
13	3, 12	wpss 3575	. . . . . . . 8 wff x C. z
14	12, 7	wpss 3575	. . . . . . . 8 wff z C. y
15	13, 14	wa 384	. . . . . . 7 wff ( x C. z /\ z C. y )
16	15, 11, 4	wrex 2913	. . . . . 6 wff E. z e. CH ( x C. z /\ z C. y )
17	16	wn 3	. . . . 5 wff -. E. z e. CH ( x C. z /\ z C. y )
18	10, 17	wa 384	. . . 4 wff ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) )
19	9, 18	wa 384	. . 3 wff ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) )
20	19, 2, 6	copab 4712	. 2 class { <. x , y >. | ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) ) }
21	1, 20	wceq 1483	1 wff <oH = { <. x , y >. | ( ( x e. CH /\ y e. CH ) /\ ( x C. y /\ -. E. z e. CH ( x C. z /\ z C. y ) ) ) }

This definition is referenced by:  cvbr  29141