Metamath Proof Explorer


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 ( ( 𝐾𝐶𝑋𝐵 ) → ( 𝑃 ∈ ( 𝑀𝑋 ) ↔ ( 𝑃𝐴𝑃 𝑋 ) ) )