# Metamath Proof Explorer

## Theorem paddss2

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

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

### Proof

Step Hyp Ref Expression
1 padd0.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
2 padd0.p
3 ssel ${⊢}{X}\subseteq {Y}\to \left({p}\in {X}\to {p}\in {Y}\right)$
4 3 orim2d ${⊢}{X}\subseteq {Y}\to \left(\left({p}\in {Z}\vee {p}\in {X}\right)\to \left({p}\in {Z}\vee {p}\in {Y}\right)\right)$
5 ssrexv ${⊢}{X}\subseteq {Y}\to \left(\exists {r}\in {X}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\to \exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)$
6 5 reximdv ${⊢}{X}\subseteq {Y}\to \left(\exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {X}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\to \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)$
7 6 anim2d ${⊢}{X}\subseteq {Y}\to \left(\left({p}\in {A}\wedge \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {X}\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 {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)$
8 4 7 orim12d ${⊢}{X}\subseteq {Y}\to \left(\left(\left({p}\in {Z}\vee {p}\in {X}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {X}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\to \left(\left({p}\in {Z}\vee {p}\in {Y}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\right)$
9 8 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 {Z}\vee {p}\in {X}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {X}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\to \left(\left({p}\in {Z}\vee {p}\in {Y}\right)\vee \left({p}\in {A}\wedge \exists {q}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {r}\in {Y}\phantom{\rule{.4em}{0ex}}{p}{\le }_{{K}}\left({q}\mathrm{join}\left({K}\right){r}\right)\right)\right)\right)$
10 simpl1 ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {K}\in {B}$
11 simpl3 ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {Z}\subseteq {A}$
12 sstr ${⊢}\left({X}\subseteq {Y}\wedge {Y}\subseteq {A}\right)\to {X}\subseteq {A}$
13 12 3ad2antr2 ${⊢}\left({X}\subseteq {Y}\wedge \left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\right)\to {X}\subseteq {A}$
14 13 ancoms ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {X}\subseteq {A}$
15 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
16 eqid ${⊢}\mathrm{join}\left({K}\right)=\mathrm{join}\left({K}\right)$
17 15 16 1 2 elpadd
18 10 11 14 17 syl3anc
19 simpl2 ${⊢}\left(\left({K}\in {B}\wedge {Y}\subseteq {A}\wedge {Z}\subseteq {A}\right)\wedge {X}\subseteq {Y}\right)\to {Y}\subseteq {A}$
20 15 16 1 2 elpadd
21 10 11 19 20 syl3anc
22 9 18 21 3imtr4d
23 22 ssrdv
24 23 ex