Theorem cdleme9taN 37424

Description: Part of proof of Lemma E in [Crawley] p. 113. 𝑋 represents t₁, which we prove is an atom. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)

Hypotheses

Ref	Expression
cdleme8t.l	⊢ ≤ = (le‘𝐾)
cdleme8t.j	⊢ ∨ = (join‘𝐾)
cdleme8t.m	⊢ ∧ = (meet‘𝐾)
cdleme8t.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme8t.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme8t.x	⊢ 𝑋 = ((𝑃 ∨ 𝑇) ∧ 𝑊)

Assertion

Ref	Expression
cdleme9taN	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑇)) → 𝑋 ∈ 𝐴)

Proof of Theorem cdleme9taN

Step	Hyp	Ref	Expression
1		cdleme8t.l	. 2 ⊢ ≤ = (le‘𝐾)
2		cdleme8t.j	. 2 ⊢ ∨ = (join‘𝐾)
3		cdleme8t.m	. 2 ⊢ ∧ = (meet‘𝐾)
4		cdleme8t.a	. 2 ⊢ 𝐴 = (Atoms‘𝐾)
5		cdleme8t.h	. 2 ⊢ 𝐻 = (LHyp‘𝐾)
6		cdleme8t.x	. 2 ⊢ 𝑋 = ((𝑃 ∨ 𝑇) ∧ 𝑊)
7	1, 2, 3, 4, 5, 6	cdleme9a 37419	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑇 ∈ 𝐴 ∧ 𝑃 ≠ 𝑇)) → 𝑋 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3016   class class class wbr 5052  ‘cfv 6341  (class class class)co 7142  lecple 16555  joincjn 17537  meetcmee 17538  Atomscatm 36431  HLchlt 36518  LHypclh 37152

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-proset 17521  df-poset 17539  df-plt 17551  df-lub 17567  df-glb 17568  df-join 17569  df-meet 17570  df-p0 17632  df-p1 17633  df-lat 17639  df-clat 17701  df-oposet 36344  df-ol 36346  df-oml 36347  df-covers 36434  df-ats 36435  df-atl 36466  df-cvlat 36490  df-hlat 36519  df-lhyp 37156

This theorem is referenced by: (None)