Metamath Proof Explorer

Theorem cvr2N

Description: Less-than and covers equivalence in a Hilbert lattice. ( chcv2 analog.) (Contributed by NM, 7-Feb-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cvr2.b ⊢ B = Base K
cvr2.s ⊢ < ˙ = < K
cvr2.j ⊢ ∨ ˙ = join ⁡ K
cvr2.c ⊢ C = ⋖ K
cvr2.a ⊢ A = Atoms ⁡ K
Assertion cvr2N ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → X < ˙ X ∨ ˙ P ↔ X C X ∨ ˙ P

Proof

Step Hyp Ref Expression
1 cvr2.b ⊢ B = Base K
2 cvr2.s ⊢ < ˙ = < K
3 cvr2.j ⊢ ∨ ˙ = join ⁡ K
4 cvr2.c ⊢ C = ⋖ K
5 cvr2.a ⊢ A = Atoms ⁡ K
6 hllat ⊢ K ∈ HL → K ∈ Lat
7 6 3ad2ant1 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → K ∈ Lat
8 simp2 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → X ∈ B
9 1 5 atbase ⊢ P ∈ A → P ∈ B
10 9 3ad2ant3 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → P ∈ B
11 eqid ⊢ ≤ K = ≤ K
12 1 11 2 3 latnle ⊢ K ∈ Lat ∧ X ∈ B ∧ P ∈ B → ¬ P ≤ K X ↔ X < ˙ X ∨ ˙ P
13 7 8 10 12 syl3anc ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → ¬ P ≤ K X ↔ X < ˙ X ∨ ˙ P
14 1 11 3 4 5 cvr1 ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → ¬ P ≤ K X ↔ X C X ∨ ˙ P
15 13 14 bitr3d ⊢ K ∈ HL ∧ X ∈ B ∧ P ∈ A → X < ˙ X ∨ ˙ P ↔ X C X ∨ ˙ P