Theorem elpmap

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

	Ref	Expression
Hypotheses	pmapfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	pmapfval.l	⊢ ≤ = ( le ‘ 𝐾 )
	pmapfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pmapfval.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
Assertion	elpmap	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pmapfval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		pmapfval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		pmapfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		pmapfval.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
5	1 2 3 4	pmapval	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑀 ‘ 𝑋 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ≤ 𝑋 } )
6	5	eleq2d	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∈ ( 𝑀 ‘ 𝑋 ) ↔ 𝑃 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ≤ 𝑋 } ) )
7		breq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋 ) )
8	7	elrab	⊢ ( 𝑃 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ≤ 𝑋 } ↔ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋 ) )
9	6 8	bitrdi	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑃 ∈ ( 𝑀 ‘ 𝑋 ) ↔ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋 ) ) )