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

Metamath Proof Explorer

Theorem dalemply

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012)

Ref Expression
Hypotheses dalema.ph ⊢ φ ↔ K ∈ HL ∧ C ∈ Base K ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ T ∈ A ∧ U ∈ A ∧ Y ∈ O ∧ Z ∈ O ∧ ¬ C ≤ ˙ P ∨ ˙ Q ∧ ¬ C ≤ ˙ Q ∨ ˙ R ∧ ¬ C ≤ ˙ R ∨ ˙ P ∧ ¬ C ≤ ˙ S ∨ ˙ T ∧ ¬ C ≤ ˙ T ∨ ˙ U ∧ ¬ C ≤ ˙ U ∨ ˙ S ∧ C ≤ ˙ P ∨ ˙ S ∧ C ≤ ˙ Q ∨ ˙ T ∧ C ≤ ˙ R ∨ ˙ U
dalemc.l ⊢ ≤ ˙ = ≤ K
dalemc.j ⊢ ∨ ˙ = join ⁡ K
dalemc.a ⊢ A = Atoms ⁡ K
dalempnes.o ⊢ O = LPlanes ⁡ K
dalempnes.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
Assertion dalemply ⊢ φ → P ≤ ˙ Y

Proof

Step Hyp Ref Expression
1 dalema.ph ⊢ φ ↔ K ∈ HL ∧ C ∈ Base K ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A ∧ S ∈ A ∧ T ∈ A ∧ U ∈ A ∧ Y ∈ O ∧ Z ∈ O ∧ ¬ C ≤ ˙ P ∨ ˙ Q ∧ ¬ C ≤ ˙ Q ∨ ˙ R ∧ ¬ C ≤ ˙ R ∨ ˙ P ∧ ¬ C ≤ ˙ S ∨ ˙ T ∧ ¬ C ≤ ˙ T ∨ ˙ U ∧ ¬ C ≤ ˙ U ∨ ˙ S ∧ C ≤ ˙ P ∨ ˙ S ∧ C ≤ ˙ Q ∨ ˙ T ∧ C ≤ ˙ R ∨ ˙ U
2 dalemc.l ⊢ ≤ ˙ = ≤ K
3 dalemc.j ⊢ ∨ ˙ = join ⁡ K
4 dalemc.a ⊢ A = Atoms ⁡ K
5 dalempnes.o ⊢ O = LPlanes ⁡ K
6 dalempnes.y ⊢ Y = P ∨ ˙ Q ∨ ˙ R
7 1 dalemkelat ⊢ φ → K ∈ Lat
8 1 4 dalempeb ⊢ φ → P ∈ Base K
9 1 dalemkehl ⊢ φ → K ∈ HL
10 1 dalemqea ⊢ φ → Q ∈ A
11 1 dalemrea ⊢ φ → R ∈ A
12 eqid ⊢ Base K = Base K
13 12 3 4 hlatjcl ⊢ K ∈ HL ∧ Q ∈ A ∧ R ∈ A → Q ∨ ˙ R ∈ Base K
14 9 10 11 13 syl3anc ⊢ φ → Q ∨ ˙ R ∈ Base K
15 12 2 3 latlej1 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∨ ˙ R ∈ Base K → P ≤ ˙ P ∨ ˙ Q ∨ ˙ R
16 7 8 14 15 syl3anc ⊢ φ → P ≤ ˙ P ∨ ˙ Q ∨ ˙ R
17 1 dalempea ⊢ φ → P ∈ A
18 3 4 hlatjass ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ R ∈ A → P ∨ ˙ Q ∨ ˙ R = P ∨ ˙ Q ∨ ˙ R
19 9 17 10 11 18 syl13anc ⊢ φ → P ∨ ˙ Q ∨ ˙ R = P ∨ ˙ Q ∨ ˙ R
20 16 19 breqtrrd ⊢ φ → P ≤ ˙ P ∨ ˙ Q ∨ ˙ R
21 20 6 breqtrrdi ⊢ φ → P ≤ ˙ Y