elpmap

	Ref	Expression
Hypotheses	pmapfval.b	$⊢ B = {Base}_{K}$
	pmapfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	pmapfval.a	$⊢ A = Atoms (K)$
	pmapfval.m	$⊢ M = pmap (K)$
Assertion	elpmap	$⊢ (K \in C \land X \in B) \to (P \in M (X) \leftrightarrow (P \in A \land P \underset{˙}{\leq} X))$

Step	Hyp	Ref	Expression
1		pmapfval.b	$⊢ B = {Base}_{K}$
2		pmapfval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		pmapfval.a	$⊢ A = Atoms (K)$
4		pmapfval.m	$⊢ M = pmap (K)$
5	1 2 3 4	pmapval	$⊢ (K \in C \land X \in B) \to M (X) = \{x \in A \| x \underset{˙}{\leq} X\}$
6	5	eleq2d	$⊢ (K \in C \land X \in B) \to (P \in M (X) \leftrightarrow P \in \{x \in A \| x \underset{˙}{\leq} X\})$
7		breq1	$⊢ x = P \to (x \underset{˙}{\leq} X \leftrightarrow P \underset{˙}{\leq} X)$
8	7	elrab	$⊢ P \in \{x \in A \| x \underset{˙}{\leq} X\} \leftrightarrow (P \in A \land P \underset{˙}{\leq} X)$
9	6 8	bitrdi	$⊢ (K \in C \land X \in B) \to (P \in M (X) \leftrightarrow (P \in A \land P \underset{˙}{\leq} X))$

Metamath Proof Explorer