![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalemkelat | Structured version Visualization version GIF version |
Description: Lemma for dath 36403. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
Ref | Expression |
---|---|
dalema.ph | ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) |
Ref | Expression |
---|---|
dalemkelat | ⊢ (𝜑 → 𝐾 ∈ Lat) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dalema.ph | . . 3 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) | |
2 | 1 | dalemkehl 36290 | . 2 ⊢ (𝜑 → 𝐾 ∈ HL) |
3 | 2 | hllatd 36031 | 1 ⊢ (𝜑 → 𝐾 ∈ Lat) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1080 ∈ wcel 2081 class class class wbr 4962 ‘cfv 6225 (class class class)co 7016 Basecbs 16312 Latclat 17484 HLchlt 36017 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-dm 5453 df-iota 6189 df-fv 6233 df-ov 7019 df-atl 35965 df-cvlat 35989 df-hlat 36018 |
This theorem is referenced by: dalemcnes 36317 dalempnes 36318 dalemqnet 36319 dalemply 36321 dalemsly 36322 dalem1 36326 dalemcea 36327 dalem3 36331 dalem4 36332 dalem5 36334 dalem8 36337 dalem-cly 36338 dalem10 36340 dalem13 36343 dalem16 36346 dalem17 36347 dalem21 36361 dalem25 36365 dalem27 36366 dalem38 36377 dalem39 36378 dalem43 36382 dalem44 36383 dalem45 36384 dalem48 36387 dalem54 36393 dalem55 36394 dalem56 36395 dalem57 36396 dalem60 36399 |
Copyright terms: Public domain | W3C validator |