Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  osumcllem10N Structured version   Visualization version   GIF version

Theorem osumcllem10N 34052
Description: Lemma for osumclN 34054. Contradict osumcllem9N 34051. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
osumcllem.l = (le‘𝐾)
osumcllem.j = (join‘𝐾)
osumcllem.a 𝐴 = (Atoms‘𝐾)
osumcllem.p + = (+𝑃𝐾)
osumcllem.o = (⊥𝑃𝐾)
osumcllem.c 𝐶 = (PSubCl‘𝐾)
osumcllem.m 𝑀 = (𝑋 + {𝑝})
osumcllem.u 𝑈 = ( ‘( ‘(𝑋 + 𝑌)))
Assertion
Ref Expression
osumcllem10N (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀𝑋)

Proof of Theorem osumcllem10N
StepHypRef Expression
1 simp11 1083 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝐾 ∈ HL)
2 simp2 1054 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑝𝐴)
32snssd 4280 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → {𝑝} ⊆ 𝐴)
4 simp12 1084 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋𝐴)
5 osumcllem.a . . . . . 6 𝐴 = (Atoms‘𝐾)
6 osumcllem.p . . . . . 6 + = (+𝑃𝐾)
75, 6sspadd2 33903 . . . . 5 ((𝐾 ∈ HL ∧ {𝑝} ⊆ 𝐴𝑋𝐴) → {𝑝} ⊆ (𝑋 + {𝑝}))
81, 3, 4, 7syl3anc 1317 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → {𝑝} ⊆ (𝑋 + {𝑝}))
9 vex 3175 . . . . 5 𝑝 ∈ V
109snss 4258 . . . 4 (𝑝 ∈ (𝑋 + {𝑝}) ↔ {𝑝} ⊆ (𝑋 + {𝑝}))
118, 10sylibr 222 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑝 ∈ (𝑋 + {𝑝}))
12 osumcllem.m . . 3 𝑀 = (𝑋 + {𝑝})
1311, 12syl6eleqr 2698 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑝𝑀)
145, 6sspadd1 33902 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → 𝑋 ⊆ (𝑋 + 𝑌))
15143ad2ant1 1074 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋 ⊆ (𝑋 + 𝑌))
16 simp3 1055 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ¬ 𝑝 ∈ (𝑋 + 𝑌))
1715, 16ssneldd 3570 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ¬ 𝑝𝑋)
18 nelne1 2877 . 2 ((𝑝𝑀 ∧ ¬ 𝑝𝑋) → 𝑀𝑋)
1913, 17, 18syl2anc 690 1 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wss 3539  {csn 4124  cfv 5789  (class class class)co 6526  lecple 15723  joincjn 16715  Atomscatm 33351  HLchlt 33438  +𝑃cpadd 33882  𝑃cpolN 33989  PSubClcpscN 34021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4711  ax-pow 4763  ax-pr 4827  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-rn 5038  df-res 5039  df-ima 5040  df-iota 5753  df-fun 5791  df-fn 5792  df-f 5793  df-f1 5794  df-fo 5795  df-f1o 5796  df-fv 5797  df-ov 6529  df-oprab 6530  df-mpt2 6531  df-1st 7036  df-2nd 7037  df-padd 33883
This theorem is referenced by:  osumcllem11N  34053
  Copyright terms: Public domain W3C validator