Metamath Proof Explorer


Theorem elpmapat

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

Ref Expression
Hypotheses pmapat.a A=AtomsK
pmapat.m M=pmapK
Assertion elpmapat KHLPAXMPX=P

Proof

Step Hyp Ref Expression
1 pmapat.a A=AtomsK
2 pmapat.m M=pmapK
3 1 2 pmapat KHLPAMP=P
4 3 eleq2d KHLPAXMPXP
5 elsn2g PAXPX=P
6 5 adantl KHLPAXPX=P
7 4 6 bitrd KHLPAXMPX=P