Theorem elpmapat

Description: Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012)

	Ref	Expression
Hypotheses	pmapat.a	|- A = ( Atoms ` K )
	pmapat.m	|- M = ( pmap ` K )
Assertion	elpmapat	|- ( ( K e. HL /\ P e. A ) -> ( X e. ( M ` P ) <-> X = P ) )

Proof

Step	Hyp	Ref	Expression
1		pmapat.a	|- A = ( Atoms ` K )
2		pmapat.m	|- M = ( pmap ` K )
3	1 2	pmapat	|- ( ( K e. HL /\ P e. A ) -> ( M ` P ) = { P } )
4	3	eleq2d	|- ( ( K e. HL /\ P e. A ) -> ( X e. ( M ` P ) <-> X e. { P } ) )
5		elsn2g	|- ( P e. A -> ( X e. { P } <-> X = P ) )
6	5	adantl	|- ( ( K e. HL /\ P e. A ) -> ( X e. { P } <-> X = P ) )
7	4 6	bitrd	|- ( ( K e. HL /\ P e. A ) -> ( X e. ( M ` P ) <-> X = P ) )