Theorem cdleme9a 40191

Description: Part of proof of Lemma E in [Crawley] p. 113. 𝐶 represents s₁, which we prove is an atom. (Contributed by NM, 10-Jun-2012.)

Hypotheses

Ref	Expression
cdleme8.l	⊢ ≤ = (le‘𝐾)
cdleme8.j	⊢ ∨ = (join‘𝐾)
cdleme8.m	⊢ ∧ = (meet‘𝐾)
cdleme8.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme8.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme8.4	⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊)

Assertion

Ref	Expression
cdleme9a	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑆)) → 𝐶 ∈ 𝐴)

Proof of Theorem cdleme9a

Step	Hyp	Ref	Expression
1		cdleme8.l	. 2 ⊢ ≤ = (le‘𝐾)
2		cdleme8.j	. 2 ⊢ ∨ = (join‘𝐾)
3		cdleme8.m	. 2 ⊢ ∧ = (meet‘𝐾)
4		cdleme8.a	. 2 ⊢ 𝐴 = (Atoms‘𝐾)
5		cdleme8.h	. 2 ⊢ 𝐻 = (LHyp‘𝐾)
6		cdleme8.4	. 2 ⊢ 𝐶 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
7	1, 2, 3, 4, 5, 6	lhpat2 39985	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑆)) → 𝐶 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107   ≠ wne 2931   class class class wbr 5116  ‘cfv 6527  (class class class)co 7399  lecple 17263  joincjn 18308  meetcmee 18309  Atomscatm 39202  HLchlt 39289  LHypclh 39924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7356  df-ov 7402  df-oprab 7403  df-proset 18291  df-poset 18310  df-plt 18325  df-lub 18341  df-glb 18342  df-join 18343  df-meet 18344  df-p0 18420  df-p1 18421  df-lat 18427  df-clat 18494  df-oposet 39115  df-ol 39117  df-oml 39118  df-covers 39205  df-ats 39206  df-atl 39237  df-cvlat 39261  df-hlat 39290  df-lhyp 39928

This theorem is referenced by:  cdleme9  40193  cdleme9taN  40196  cdleme11h  40206  cdleme11j  40207  cdleme11k  40208  cdleme17c  40228