Metamath Proof Explorer

Theorem cvlatcvr2

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

Ref Expression
Hypotheses cvlatcvr1.j ⊢ ∨ ˙ = join ⁡ K
cvlatcvr1.c ⊢ C = ⋖ K
cvlatcvr1.a ⊢ A = Atoms ⁡ K
Assertion cvlatcvr2 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C Q ∨ ˙ P

Proof

Step Hyp Ref Expression
1 cvlatcvr1.j ⊢ ∨ ˙ = join ⁡ K
2 cvlatcvr1.c ⊢ C = ⋖ K
3 cvlatcvr1.a ⊢ A = Atoms ⁡ K
4 1 2 3 cvlatcvr1 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C P ∨ ˙ Q
5 simp13 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → K ∈ CvLat
6 cvllat ⊢ K ∈ CvLat → K ∈ Lat
7 5 6 syl ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → K ∈ Lat
8 eqid ⊢ Base K = Base K
9 8 3 atbase ⊢ P ∈ A → P ∈ Base K
10 9 3ad2ant2 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ∈ Base K
11 8 3 atbase ⊢ Q ∈ A → Q ∈ Base K
12 11 3ad2ant3 ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → Q ∈ Base K
13 8 1 latjcom ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K → P ∨ ˙ Q = Q ∨ ˙ P
14 7 10 12 13 syl3anc ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q = Q ∨ ˙ P
15 14 breq2d ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P C P ∨ ˙ Q ↔ P C Q ∨ ˙ P
16 4 15 bitrd ⊢ K ∈ OML ∧ K ∈ CLat ∧ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A → P ≠ Q ↔ P C Q ∨ ˙ P