Definition df-cv 30641

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 𝐴 ⋖_ℋ 𝐵 is read "𝐵 covers 𝐴 " or "𝐴 is covered by 𝐵 " , and it means that 𝐵 is larger than 𝐴 and there is nothing in between. See cvbr 30644 and cvbr2 30645 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.)

Assertion

Ref	Expression
df-cv	⊢ ⋖ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))}

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cv

Step	Hyp	Ref	Expression
1		ccv 29326	. 2 class ⋖ℋ
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1538	. . . . . 6 class 𝑥
4		cch 29291	. . . . . 6 class Cℋ
5	3, 4	wcel 2106	. . . . 5 wff 𝑥 ∈ Cℋ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1538	. . . . . 6 class 𝑦
8	7, 4	wcel 2106	. . . . 5 wff 𝑦 ∈ Cℋ
9	5, 8	wa 396	. . . 4 wff (𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ )
10	3, 7	wpss 3888	. . . . 5 wff 𝑥 ⊊ 𝑦
11		vz	. . . . . . . . . 10 setvar 𝑧
12	11	cv 1538	. . . . . . . . 9 class 𝑧
13	3, 12	wpss 3888	. . . . . . . 8 wff 𝑥 ⊊ 𝑧
14	12, 7	wpss 3888	. . . . . . . 8 wff 𝑧 ⊊ 𝑦
15	13, 14	wa 396	. . . . . . 7 wff (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)
16	15, 11, 4	wrex 3065	. . . . . 6 wff ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)
17	16	wn 3	. . . . 5 wff ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)
18	10, 17	wa 396	. . . 4 wff (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦))
19	9, 18	wa 396	. . 3 wff ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))
20	19, 2, 6	copab 5136	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))}
21	1, 20	wceq 1539	1 wff ⋖ℋ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))}

This definition is referenced by:  cvbr  30644