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

Metamath Proof Explorer

Theorem cvlexch4N

Description: An atomic covering lattice has the exchange property. Part of Definition 7.8 of MaedaMaeda p. 32. (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cvlexch3.b ⊢ B = Base K
cvlexch3.l ⊢ ≤ ˙ = ≤ K
cvlexch3.j ⊢ ∨ ˙ = join ⁡ K
cvlexch3.m ⊢ ∧ ˙ = meet ⁡ K
cvlexch3.z ⊢ 0 ˙ = 0. ⁡ K
cvlexch3.a ⊢ A = Atoms ⁡ K
Assertion cvlexch4N ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B ∧ P ∧ ˙ X = 0 ˙ → P ≤ ˙ X ∨ ˙ Q ↔ X ∨ ˙ P = X ∨ ˙ Q

Proof

Step Hyp Ref Expression
1 cvlexch3.b ⊢ B = Base K
2 cvlexch3.l ⊢ ≤ ˙ = ≤ K
3 cvlexch3.j ⊢ ∨ ˙ = join ⁡ K
4 cvlexch3.m ⊢ ∧ ˙ = meet ⁡ K
5 cvlexch3.z ⊢ 0 ˙ = 0. ⁡ K
6 cvlexch3.a ⊢ A = Atoms ⁡ K
7 cvlatl ⊢ K ∈ CvLat → K ∈ AtLat
8 7 adantr ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B → K ∈ AtLat
9 simpr1 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B → P ∈ A
10 simpr3 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B → X ∈ B
11 1 2 4 5 6 atnle ⊢ K ∈ AtLat ∧ P ∈ A ∧ X ∈ B → ¬ P ≤ ˙ X ↔ P ∧ ˙ X = 0 ˙
12 8 9 10 11 syl3anc ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B → ¬ P ≤ ˙ X ↔ P ∧ ˙ X = 0 ˙
13 1 2 3 6 cvlexchb1 ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B ∧ ¬ P ≤ ˙ X → P ≤ ˙ X ∨ ˙ Q ↔ X ∨ ˙ P = X ∨ ˙ Q
14 13 3expia ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B → ¬ P ≤ ˙ X → P ≤ ˙ X ∨ ˙ Q ↔ X ∨ ˙ P = X ∨ ˙ Q
15 12 14 sylbird ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B → P ∧ ˙ X = 0 ˙ → P ≤ ˙ X ∨ ˙ Q ↔ X ∨ ˙ P = X ∨ ˙ Q
16 15 3impia ⊢ K ∈ CvLat ∧ P ∈ A ∧ Q ∈ A ∧ X ∈ B ∧ P ∧ ˙ X = 0 ˙ → P ≤ ˙ X ∨ ˙ Q ↔ X ∨ ˙ P = X ∨ ˙ Q