Theorem hlcvl 40523

Description: A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)

Assertion

Ref	Expression
hlcvl	⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)

Proof of Theorem hlcvl

Step	Hyp	Ref	Expression
1		hlomcmcv 40520	. 2 ⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat))
2	1	simp3d 1162	1 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  CLatccla 18679  OMLcoml 40339  CvLatclc 40429  HLchlt 40514

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6496  df-fv 6549  df-ov 7425  df-hlat 40515

This theorem is used by:  hlatl  40524  hlexch1  40546  hlexch2  40547  hlexchb1  40548  hlexchb2  40549  hlsupr2  40551  hlexch3  40555  hlexch4N  40556  hlatexchb1  40557  hlatexchb2  40558  hlatexch1  40559  hlatexch2  40560  llnexchb2lem  41032  4atexlemkc  41222  4atex  41240  4atex3  41245  cdleme02N  41386  cdleme0ex2N  41388  cdleme0moN  41389  cdleme0nex  41454  cdleme20zN  41465  cdleme19a  41467  cdleme19d  41470  cdleme21a  41489  cdleme21b  41490  cdleme21c  41491  cdleme21ct  41493  cdleme22f  41510  cdleme22f2  41511  cdleme22g  41512  cdlemf1  41725