Theorem paddunssN

Description: Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
Assertion	paddunssN	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\cup Y\subseteq X\underset{\dot{}}{+}Y$$

Proof

Step	Hyp	Ref	Expression
1		padd0.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		padd0.p	$$⊢\underset{\dot{}}{+}={+}_{𝑃}\left(K\right)$$
3		ssun1	$$⊢X\cup Y\subseteq \left(X\cup Y\right)\cup \left\{p\in A|\exists q\in X\exists r\in Yp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
4		eqid	$$⊢{\le }_K={\le }_K$$
5		eqid	$$⊢\mathrm{join}\left(K\right)=\mathrm{join}\left(K\right)$$
6	4 5 1 2	paddval	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\underset{\dot{}}{+}Y=\left(X\cup Y\right)\cup \left\{p\in A|\exists q\in X\exists r\in Yp{\le }_K\left(q\mathrm{join}\left(K\right)r\right)\right\}$$
7	3 6	sseqtrrid	$$⊢\left(K\in B\wedge X\subseteq A\wedge Y\subseteq A\right)\to X\cup Y\subseteq X\underset{\dot{}}{+}Y$$