![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > hlcvl | Structured version Visualization version GIF version |
Description: A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
Ref | Expression |
---|---|
hlcvl | ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlomcmcv 35426 | . 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat)) | |
2 | 1 | simp3d 1178 | 1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2164 CLatccla 17467 OMLcoml 35245 CvLatclc 35335 HLchlt 35420 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-ral 3122 df-rex 3123 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4147 df-if 4309 df-sn 4400 df-pr 4402 df-op 4406 df-uni 4661 df-br 4876 df-iota 6090 df-fv 6135 df-ov 6913 df-hlat 35421 |
This theorem is referenced by: hlatl 35430 hlexch1 35452 hlexch2 35453 hlexchb1 35454 hlexchb2 35455 hlsupr2 35457 hlexch3 35461 hlexch4N 35462 hlatexchb1 35463 hlatexchb2 35464 hlatexch1 35465 hlatexch2 35466 llnexchb2lem 35938 4atexlemkc 36128 4atex 36146 4atex3 36151 cdleme02N 36292 cdleme0ex2N 36294 cdleme0moN 36295 cdleme0nex 36360 cdleme20zN 36371 cdleme19a 36373 cdleme19d 36376 cdleme21a 36395 cdleme21b 36396 cdleme21c 36397 cdleme21ct 36399 cdleme22f 36416 cdleme22f2 36417 cdleme22g 36418 cdlemf1 36631 |
Copyright terms: Public domain | W3C validator |