This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℋ ( 𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦 ) ) ) }