Theorem elpmap

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

	Ref	Expression
Hypotheses	pmapfval.b	$$⊢B={\mathrm{Base}}_K$$
	pmapfval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	pmapfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pmapfval.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	elpmap	$$⊢\left(K\in C\wedge X\in B\right)\to \left(P\in M\left(X\right)\leftrightarrow \left(P\in A\wedge P\underset{\dot{}}{\le }X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmapfval.b	$$⊢B={\mathrm{Base}}_K$$
2		pmapfval.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		pmapfval.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		pmapfval.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
5	1 2 3 4	pmapval	$$⊢\left(K\in C\wedge X\in B\right)\to M\left(X\right)=\left\{x\in A|x\underset{\dot{}}{\le }X\right\}$$
6	5	eleq2d	$$⊢\left(K\in C\wedge X\in B\right)\to \left(P\in M\left(X\right)\leftrightarrow P\in \left\{x\in A|x\underset{\dot{}}{\le }X\right\}\right)$$
7		breq1	$$⊢x=P\to \left(x\underset{\dot{}}{\le }X\leftrightarrow P\underset{\dot{}}{\le }X\right)$$
8	7	elrab	$$⊢P\in \left\{x\in A|x\underset{\dot{}}{\le }X\right\}\leftrightarrow \left(P\in A\wedge P\underset{\dot{}}{\le }X\right)$$
9	6 8	bitrdi	$$⊢\left(K\in C\wedge X\in B\right)\to \left(P\in M\left(X\right)\leftrightarrow \left(P\in A\wedge P\underset{\dot{}}{\le }X\right)\right)$$