Theorem elpmap

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

	Ref	Expression
Hypotheses	pmapfval.b	|- B = ( Base ` K )
	pmapfval.l	|- .<_ = ( le ` K )
	pmapfval.a	|- A = ( Atoms ` K )
	pmapfval.m	|- M = ( pmap ` K )
Assertion	elpmap	|- ( ( K e. C /\ X e. B ) -> ( P e. ( M ` X ) <-> ( P e. A /\ P .<_ X ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmapfval.b	|- B = ( Base ` K )
2		pmapfval.l	|- .<_ = ( le ` K )
3		pmapfval.a	|- A = ( Atoms ` K )
4		pmapfval.m	|- M = ( pmap ` K )
5	1 2 3 4	pmapval	|- ( ( K e. C /\ X e. B ) -> ( M ` X ) = { x e. A | x .<_ X } )
6	5	eleq2d	|- ( ( K e. C /\ X e. B ) -> ( P e. ( M ` X ) <-> P e. { x e. A | x .<_ X } ) )
7		breq1	|- ( x = P -> ( x .<_ X <-> P .<_ X ) )
8	7	elrab	|- ( P e. { x e. A | x .<_ X } <-> ( P e. A /\ P .<_ X ) )
9	6 8	bitrdi	|- ( ( K e. C /\ X e. B ) -> ( P e. ( M ` X ) <-> ( P e. A /\ P .<_ X ) ) )