Theorem elpmapat

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

	Ref	Expression
Hypotheses	pmapat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	pmapat.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
Assertion	elpmapat	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \left(X\in M\left(P\right)\leftrightarrow X=P\right)$$

Proof

Step	Hyp	Ref	Expression
1		pmapat.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
2		pmapat.m	$$⊢M=\mathrm{pmap}\left(K\right)$$
3	1 2	pmapat	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to M\left(P\right)=\left\{P\right\}$$
4	3	eleq2d	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \left(X\in M\left(P\right)\leftrightarrow X\in \left\{P\right\}\right)$$
5		elsn2g	$$⊢P\in A\to \left(X\in \left\{P\right\}\leftrightarrow X=P\right)$$
6	5	adantl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \left(X\in \left\{P\right\}\leftrightarrow X=P\right)$$
7	4 6	bitrd	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\right)\to \left(X\in M\left(P\right)\leftrightarrow X=P\right)$$