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 = ( Base ` K )
	pmapssba.m	|- M = ( pmap ` K )
Assertion	pmapssbaN	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) C_ B )

Proof

Step	Hyp	Ref	Expression
1		pmapssba.b	|- B = ( Base ` K )
2		pmapssba.m	|- M = ( pmap ` K )
3		eqid	|- ( Atoms ` K ) = ( Atoms ` K )
4	1 3 2	pmapssat	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) C_ ( Atoms ` K ) )
5	1 3	atssbase	|- ( Atoms ` K ) C_ B
6	4 5	sstrdi	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) C_ B )