HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-cv Unicode version

Definition df-cv 22689
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 22692 and cvbr2 22693 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
StepHypRef Expression
1 ccv 21374 . 2  class  <oH
2 vx . . . . . . 7  set  x
32cv 1618 . . . . . 6  class  x
4 cch 21339 . . . . . 6  class  CH
53, 4wcel 1621 . . . . 5  wff  x  e. 
CH
6 vy . . . . . . 7  set  y
76cv 1618 . . . . . 6  class  y
87, 4wcel 1621 . . . . 5  wff  y  e. 
CH
95, 8wa 360 . . . 4  wff  ( x  e.  CH  /\  y  e.  CH )
103, 7wpss 3079 . . . . 5  wff  x  C.  y
11 vz . . . . . . . . . 10  set  z
1211cv 1618 . . . . . . . . 9  class  z
133, 12wpss 3079 . . . . . . . 8  wff  x  C.  z
1412, 7wpss 3079 . . . . . . . 8  wff  z  C.  y
1513, 14wa 360 . . . . . . 7  wff  ( x 
C.  z  /\  z  C.  y )
1615, 11, 4wrex 2510 . . . . . 6  wff  E. z  e.  CH  ( x  C.  z  /\  z  C.  y
)
1716wn 5 . . . . 5  wff  -.  E. z  e.  CH  ( x 
C.  z  /\  z  C.  y )
1810, 17wa 360 . . . 4  wff  ( x 
C.  y  /\  -.  E. z  e.  CH  (
x  C.  z  /\  z  C.  y ) )
199, 18wa 360 . . 3  wff  ( ( x  e.  CH  /\  y  e.  CH )  /\  ( x  C.  y  /\  -.  E. z  e. 
CH  ( x  C.  z  /\  z  C.  y
) ) )
2019, 2, 6copab 3973 . 2  class  { <. x ,  y >.  |  ( ( x  e.  CH  /\  y  e.  CH )  /\  ( x  C.  y  /\  -.  E. z  e. 
CH  ( x  C.  z  /\  z  C.  y
) ) ) }
211, 20wceq 1619 1  wff  <oH  =  { <. x ,  y >.  |  ( ( x  e.  CH  /\  y  e.  CH )  /\  (
x  C.  y  /\  -.  E. z  e.  CH  ( x  C.  z  /\  z  C.  y ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  cvbr  22692
  Copyright terms: Public domain W3C validator