Theorem pmapssat

Description: The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012)

	Ref	Expression
Hypotheses	pmapssat.b	|- B = ( Base ` K )
	pmapssat.a	|- A = ( Atoms ` K )
	pmapssat.m	|- M = ( pmap ` K )
Assertion	pmapssat	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		pmapssat.b	|- B = ( Base ` K )
2		pmapssat.a	|- A = ( Atoms ` K )
3		pmapssat.m	|- M = ( pmap ` K )
4		eqid	|- ( le ` K ) = ( le ` K )
5	1 4 2 3	pmapval	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) = { p e. A | p ( le ` K ) X } )
6		ssrab2	|- { p e. A | p ( le ` K ) X } C_ A
7	5 6	eqsstrdi	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) C_ A )