Theorem pmapssbaN

Description: A weakening of pmapssat to shorten some proofs. (Contributed by NM, 7-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pmapssba.b	$$⊢B={\mathrm{Base}}_K$$
	pmapssba.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	pmapssbaN	$$⊢\left(K\in C\wedge X\in B\right)\to M\left(X\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		pmapssba.b	$$⊢B={\mathrm{Base}}_K$$
2		pmapssba.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
3		eqid	$$⊢\mathrm{Atoms}\left(K\right)=\mathrm{Atoms}\left(K\right)$$
4	1 3 2	pmapssat	$$⊢\left(K\in C\wedge X\in B\right)\to M\left(X\right)\subseteq \mathrm{Atoms}\left(K\right)$$
5	1 3	atssbase	$$⊢\mathrm{Atoms}\left(K\right)\subseteq B$$
6	4 5	sstrdi	$$⊢\left(K\in C\wedge X\in B\right)\to M\left(X\right)\subseteq B$$