# Metamath Proof Explorer

Description: Subset law for projective subspace sum. ( unss1 analog.) (Contributed by NM, 7-Mar-2012)

Ref Expression
Hypotheses padd0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$

### Proof

Step Hyp Ref Expression
1 padd0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
3 ssel ${⊢}{X}\subseteq {Y}\to \left({p}\in {X}\to {p}\in {Y}\right)$
4 3 orim1d ${⊢}{X}\subseteq {Y}\to \left(\left({p}\in {X}\vee {p}\in {Z}\right)\to \left({p}\in {Y}\vee {p}\in {Z}\right)\right)$
5 ssrexv ${⊢}{X}\subseteq {Y}\to \left(\exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\to \exists {q}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)$
6 5 anim2d ${⊢}{X}\subseteq {Y}\to \left(\left({p}\in {A}\wedge \exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\to \left({p}\in {A}\wedge \exists {q}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)$
7 4 6 orim12d ${⊢}{X}\subseteq {Y}\to \left(\left(\left({p}\in {X}\vee {p}\in {Z}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\to \left(\left({p}\in {Y}\vee {p}\in {Z}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\right)$
8 7 adantl ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to \left(\left(\left({p}\in {X}\vee {p}\in {Z}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {X}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\to \left(\left({p}\in {Y}\vee {p}\in {Z}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {Y}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Z}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\right)$
9 simpl1 ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {K}\in {B}$
10 sstr ${⊢}\left({X}\subseteq {Y}\wedge {Y}\subseteq {A}\right)\to {X}\subseteq {A}$
11 10 3ad2antr2 ${⊢}\left({X}\subseteq {Y}\wedge \left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\to {X}\subseteq {A}$
12 11 ancoms ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {X}\subseteq {A}$
13 simpl3 ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {Z}\subseteq {A}$
14 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
15 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
16 14 15 1 2 elpadd
17 9 12 13 16 syl3anc
18 14 15 1 2 elpadd