Metamath Proof Explorer


Theorem elpmap

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

Ref Expression
Hypotheses pmapfval.b B = Base K
pmapfval.l ˙ = K
pmapfval.a A = Atoms K
pmapfval.m M = pmap K
Assertion elpmap K C X B P M X P A P ˙ X

Proof

Step Hyp Ref Expression
1 pmapfval.b B = Base K
2 pmapfval.l ˙ = K
3 pmapfval.a A = Atoms K
4 pmapfval.m M = pmap K
5 1 2 3 4 pmapval K C X B M X = x A | x ˙ X
6 5 eleq2d K C X B P M X P x A | x ˙ X
7 breq1 x = P x ˙ X P ˙ X
8 7 elrab P x A | x ˙ X P A P ˙ X
9 6 8 bitrdi K C X B P M X P A P ˙ X