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 34909

Description: Lemma for dath 35022. 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 1172	. 2 ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → 𝐾 ∈ HL)
3	1, 2	sylbi 207	1 ⊢ (𝜑 → 𝐾 ∈ HL)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 ∈ wcel 1990 class class class wbr 4653 ‘cfv 5888 (class class class)co 6650 Basecbs 15857 HLchlt 34637

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 197 df-an 386 df-3an 1039

This theorem is referenced by: dalemkelat 34910 dalemkeop 34911 dalempjqeb 34931 dalemsjteb 34932 dalemtjueb 34933 dalemqrprot 34934 dalempnes 34937 dalemqnet 34938 dalempjsen 34939 dalemply 34940 dalemsly 34941 dalemswapyz 34942 dalemrot 34943 dalemrotyz 34944 dalem1 34945 dalemcea 34946 dalem2 34947 dalemdea 34948 dalem3 34950 dalem4 34951 dalem5 34953 dalem-cly 34957 dalem9 34958 dalem11 34960 dalem12 34961 dalem13 34962 dalem15 34964 dalem16 34965 dalem17 34966 dalem18 34967 dalem19 34968 dalemswapyzps 34976 dalemcjden 34978 dalem21 34980 dalem22 34981 dalem23 34982 dalem24 34983 dalem25 34984 dalem27 34985 dalem28 34986 dalem38 34996 dalem39 34997 dalem41 34999 dalem42 35000 dalem43 35001 dalem44 35002 dalem45 35003 dalem51 35009 dalem52 35010 dalem54 35012 dalem55 35013 dalem56 35014 dalem57 35015 dalem58 35016 dalem59 35017 dalem60 35018

W3C validator