Metamath Proof Explorer

Theorem atcvr1

Description: An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses atcvr1.j ⊢ ∨ ˙ = join ⁡ K
atcvr1.c ⊢ C = ⋖ K
atcvr1.a ⊢ A = Atoms ⁡ K
Assertion atcvr1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q

Proof

Step Hyp Ref Expression
1 atcvr1.j ⊢ ∨ ˙ = join ⁡ K
2 atcvr1.c ⊢ C = ⋖ K
3 atcvr1.a ⊢ A = Atoms ⁡ K
4 hlomcmcv ⊢ K ∈ HL → K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat
5 1 2 3 cvlatcvr1 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q
6 4 5 syl3an1 ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q