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	$$⊢{⋖}_{\mathscr{H}}=\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(x\subset y\wedge \neg \exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccv	$$class{⋖}_{\mathscr{H}}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4		cch	$$class{\mathbf{C}}_{\mathscr{H}}$$
5	3 4	wcel	$$wffx\in {\mathbf{C}}_{\mathscr{H}}$$
6	2	cv	$$setvary$$
7	6 4	wcel	$$wffy\in {\mathbf{C}}_{\mathscr{H}}$$
8	5 7	wa	$$wff\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)$$
9	3 6	wpss	$$wffx\subset y$$
10		vz	$$setvarz$$
11	10	cv	$$setvarz$$
12	3 11	wpss	$$wffx\subset z$$
13	11 6	wpss	$$wffz\subset y$$
14	12 13	wa	$$wff\left(x\subset z\wedge z\subset y\right)$$
15	14 10 4	wrex	$$wff\exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)$$
16	15	wn	$$wff\neg \exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)$$
17	9 16	wa	$$wff\left(x\subset y\wedge \neg \exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)\right)$$
18	8 17	wa	$$wff\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(x\subset y\wedge \neg \exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)\right)\right)$$
19	18 1 2	copab	$$class\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(x\subset y\wedge \neg \exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)\right)\right)\right\}$$
20	0 19	wceq	$$wff{⋖}_{\mathscr{H}}=\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \left(x\subset y\wedge \neg \exists z\in {\mathbf{C}}_{\mathscr{H}}\left(x\subset z\wedge z\subset y\right)\right)\right)\right\}$$