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	⊢ ⋖ℋ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ( 𝑥 ⊊ 𝑦 ∧ ¬ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccv	⊢ ⋖ℋ
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cch	⊢ Cℋ
5	3 4	wcel	⊢ 𝑥 ∈ Cℋ
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ Cℋ
8	5 7	wa	⊢ ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ )
9	3 6	wpss	⊢ 𝑥 ⊊ 𝑦
10		vz	⊢ 𝑧
11	10	cv	⊢ 𝑧
12	3 11	wpss	⊢ 𝑥 ⊊ 𝑧
13	11 6	wpss	⊢ 𝑧 ⊊ 𝑦
14	12 13	wa	⊢ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 )
15	14 10 4	wrex	⊢ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 )
16	15	wn	⊢ ¬ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 )
17	9 16	wa	⊢ ( 𝑥 ⊊ 𝑦 ∧ ¬ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 ) )
18	8 17	wa	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ( 𝑥 ⊊ 𝑦 ∧ ¬ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 ) ) )
19	18 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ( 𝑥 ⊊ 𝑦 ∧ ¬ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 ) ) ) }
20	0 19	wceq	⊢ ⋖ℋ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ( 𝑥 ⊊ 𝑦 ∧ ¬ ∃ 𝑧 ∈ Cℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 ) ) ) }