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

Metamath Proof Explorer

Theorem dalempjqeb

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
dalemb.j ⊢ ∨ ˙ = join ⁡ K
dalemb.a ⊢ A = Atoms ⁡ K
Assertion dalempjqeb ⊢ φ → P ∨ ˙ Q ∈ Base K

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 dalemb.j ⊢ ∨ ˙ = join ⁡ K
3 dalemb.a ⊢ A = Atoms ⁡ K
4 1 dalemkehl ⊢ φ → K ∈ HL
5 1 dalempea ⊢ φ → P ∈ A
6 1 dalemqea ⊢ φ → Q ∈ A
7 eqid ⊢ Base K = Base K
8 7 2 3 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
9 4 5 6 8 syl3anc ⊢ φ → P ∨ ˙ Q ∈ Base K