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

Metamath Proof Explorer

Theorem dalemsly

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 15-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
dalemsly.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
Assertion dalemsly ⊢ φ ∧ Y = Z → S ≤ ˙ 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 dalemsly.z ⊢ Z = S ∨ ˙ T ∨ ˙ U
6 1 dalemkelat ⊢ φ → K ∈ Lat
7 1 4 dalemseb ⊢ φ → S ∈ Base K
8 1 3 4 dalemtjueb ⊢ φ → T ∨ ˙ U ∈ Base K
9 eqid ⊢ Base K = Base K
10 9 2 3 latlej1 ⊢ K ∈ Lat ∧ S ∈ Base K ∧ T ∨ ˙ U ∈ Base K → S ≤ ˙ S ∨ ˙ T ∨ ˙ U
11 6 7 8 10 syl3anc ⊢ φ → S ≤ ˙ S ∨ ˙ T ∨ ˙ U
12 1 dalemkehl ⊢ φ → K ∈ HL
13 1 dalemsea ⊢ φ → S ∈ A
14 1 dalemtea ⊢ φ → T ∈ A
15 1 dalemuea ⊢ φ → U ∈ A
16 3 4 hlatjass ⊢ K ∈ HL ∧ S ∈ A ∧ T ∈ A ∧ U ∈ A → S ∨ ˙ T ∨ ˙ U = S ∨ ˙ T ∨ ˙ U
17 12 13 14 15 16 syl13anc ⊢ φ → S ∨ ˙ T ∨ ˙ U = S ∨ ˙ T ∨ ˙ U
18 11 17 breqtrrd ⊢ φ → S ≤ ˙ S ∨ ˙ T ∨ ˙ U
19 18 5 breqtrrdi ⊢ φ → S ≤ ˙ Z
20 19 adantr ⊢ φ ∧ Y = Z → S ≤ ˙ Z
21 simpr ⊢ φ ∧ Y = Z → Y = Z
22 20 21 breqtrrd ⊢ φ ∧ Y = Z → S ≤ ˙ Y