Theorem elpmapat

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

	Ref	Expression
Hypotheses	pmapat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmapat.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	elpmapat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∈ ( 𝑀 ‘ 𝑃 ) ↔ 𝑋 = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		pmapat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pmapat.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
3	1 2	pmapat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑀 ‘ 𝑃 ) = { 𝑃 } )
4	3	eleq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∈ ( 𝑀 ‘ 𝑃 ) ↔ 𝑋 ∈ { 𝑃 } ) )
5		elsn2g	⊢ ( 𝑃 ∈ 𝐴 → ( 𝑋 ∈ { 𝑃 } ↔ 𝑋 = 𝑃 ) )
6	5	adantl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∈ { 𝑃 } ↔ 𝑋 = 𝑃 ) )
7	4 6	bitrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∈ ( 𝑀 ‘ 𝑃 ) ↔ 𝑋 = 𝑃 ) )