# Metamath Proof Explorer

## Theorem osumcllem1N

Description: Lemma for osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

Ref Expression
Hypotheses osumcllem.l
osumcllem.j
osumcllem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
osumcllem.p
osumcllem.o
osumcllem.c ${⊢}{C}=\mathrm{PSubCl}\left({K}\right)$
osumcllem.m
osumcllem.u
Assertion osumcllem1N ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {U}\cap {M}={M}$

### Proof

Step Hyp Ref Expression
1 osumcllem.l
2 osumcllem.j
3 osumcllem.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
4 osumcllem.p
5 osumcllem.o
6 osumcllem.c ${⊢}{C}=\mathrm{PSubCl}\left({K}\right)$
7 osumcllem.m
8 osumcllem.u
11 simpl1 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {K}\in \mathrm{HL}$
14 3 5 2polssN
15 11 13 14 syl2anc
16 15 8 sseqtrrdi
17 10 16 sstrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {X}\subseteq {U}$
18 simpr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {p}\in {U}$
19 18 snssd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to \left\{{p}\right\}\subseteq {U}$
20 simpl2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {X}\subseteq {A}$
21 3 5 polssatN
22 11 13 21 syl2anc
23 3 5 polssatN
24 11 22 23 syl2anc
25 8 24 eqsstrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {U}\subseteq {A}$
26 19 25 sstrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to \left\{{p}\right\}\subseteq {A}$
27 eqid ${⊢}\mathrm{PSubSp}\left({K}\right)=\mathrm{PSubSp}\left({K}\right)$
28 3 27 5 polsubN
29 11 22 28 syl2anc
30 8 29 eqeltrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {U}\in \mathrm{PSubSp}\left({K}\right)$
34 7 33 eqsstrid ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {M}\subseteq {U}$
35 sseqin2 ${⊢}{M}\subseteq {U}↔{U}\cap {M}={M}$
36 34 35 sylib ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {X}\subseteq {A}\wedge {Y}\subseteq {A}\right)\wedge {p}\in {U}\right)\to {U}\cap {M}={M}$