Theorem cvlatl 39444

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

Assertion

Ref	Expression
cvlatl	⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)

Proof of Theorem cvlatl

Dummy variables 𝑞 𝑝 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2733	. . 3 ⊢ (Base‘𝐾) = (Base‘𝐾)
2		eqid 2733	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
3		eqid 2733	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
4		eqid 2733	. . 3 ⊢ (Atoms‘𝐾) = (Atoms‘𝐾)
5	1, 2, 3, 4	iscvlat 39442	. 2 ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ (Atoms‘𝐾)∀𝑞 ∈ (Atoms‘𝐾)∀𝑥 ∈ (Base‘𝐾)((¬ 𝑝(le‘𝐾)𝑥 ∧ 𝑝(le‘𝐾)(𝑥(join‘𝐾)𝑞)) → 𝑞(le‘𝐾)(𝑥(join‘𝐾)𝑝))))
6	5	simplbi 497	1 ⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2113  ∀wral 3048   class class class wbr 5093  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  lecple 17170  joincjn 18219  Atomscatm 39382  AtLatcal 39383  CvLatclc 39384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-cvlat 39441

This theorem is referenced by:  cvllat  39445  cvlexch3  39451  cvlexch4N  39452  cvlatexchb1  39453  cvlcvr1  39458  cvlcvrp  39459  cvlatcvr1  39460  cvlsupr2  39462  hlatl  39479