Definition df-cv 5712

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 ⋖ 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 cvbrt 5714 and cvbr2t 5715 for membership relations.

Assertion

Ref	Expression
df-cv	⊢ ⋖ = {⟨x, y⟩∣((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ (x ⊂ y ∧ ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-cv

Step	Hyp	Ref	Expression
1		ccv 4981	. 2 class ⋖
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cch 4968	. . . . . 6 class Cℋ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ Cℋ
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y ∈ Cℋ
9	5, 8	wa 196	. . . 4 wff (x ∈ Cℋ ∧ y ∈ Cℋ )
10	3, 7	wpss 1488	. . . . 5 wff x ⊂ y
11		vz	. . . . . . . . . 10 set z
12	11	cv 1089	. . . . . . . . 9 class z
13	3, 12	wpss 1488	. . . . . . . 8 wff x ⊂ z
14	12, 7	wpss 1488	. . . . . . . 8 wff z ⊂ y
15	13, 14	wa 196	. . . . . . 7 wff (x ⊂ z ∧ z ⊂ y)
16	15, 11, 4	wrex 1202	. . . . . 6 wff ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)
17	16	wn 1	. . . . 5 wff ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)
18	10, 17	wa 196	. . . 4 wff (x ⊂ y ∧ ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y))
19	9, 18	wa 196	. . 3 wff ((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ (x ⊂ y ∧ ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)))
20	19, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ (x ⊂ y ∧ ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)))}
21	1, 20	wceq 1091	1 wff ⋖ = {⟨x, y⟩∣((x ∈ Cℋ ∧ y ∈ Cℋ ) ∧ (x ⊂ y ∧ ¬ ∃z ∈ Cℋ (x ⊂ z ∧ z ⊂ y)))}

This definition is referenced by:  cvbrt 5714

metamath.org