dalemkehl - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalemkehl		Structured version Visualization version GIF version

Theorem dalemkehl 35648

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

**Hypothesis**
Ref	Expression
dalema.ph	⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))

**Assertion**
Ref	Expression
dalemkehl	⊢ (𝜑 → 𝐾 ∈ HL)

**Proof of Theorem dalemkehl**
Step	Hyp	Ref	Expression
1		dalema.ph	. 2 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))
2		simp11l 1384	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → 𝐾 ∈ HL)
3	1, 2	sylbi 209	1 ⊢ (𝜑 → 𝐾 ∈ HL)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 385 ∧ w3a 1108 ∈ wcel 2157 class class class wbr 4847 ‘cfv 6105 (class class class)co 6882 Basecbs 16188 HLchlt 35375

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8

This theorem depends on definitions: df-bi 199 df-an 386 df-3an 1110

This theorem is referenced by: dalemkelat 35649 dalemkeop 35650 dalempjqeb 35670 dalemsjteb 35671 dalemtjueb 35672 dalemqrprot 35673 dalempnes 35676 dalemqnet 35677 dalempjsen 35678 dalemply 35679 dalemsly 35680 dalemswapyz 35681 dalemrot 35682 dalemrotyz 35683 dalem1 35684 dalemcea 35685 dalem2 35686 dalemdea 35687 dalem3 35689 dalem4 35690 dalem5 35692 dalem-cly 35696 dalem9 35697 dalem11 35699 dalem12 35700 dalem13 35701 dalem15 35703 dalem16 35704 dalem17 35705 dalem18 35706 dalem19 35707 dalemswapyzps 35715 dalemcjden 35717 dalem21 35719 dalem22 35720 dalem23 35721 dalem24 35722 dalem25 35723 dalem27 35724 dalem28 35725 dalem38 35735 dalem39 35736 dalem41 35738 dalem42 35739 dalem43 35740 dalem44 35741 dalem45 35742 dalem51 35748 dalem52 35749 dalem54 35751 dalem55 35752 dalem56 35753 dalem57 35754 dalem58 35755 dalem59 35756 dalem60 35757

W3C validator