df-pmap

Description: Define projective map for k at a . Definition in Theorem 15.5 of MaedaMaeda p. 62. (Contributed by NM, 2-Oct-2011)

		Ref	Expression
	Assertion	df-pmap	$⊢ pmap = (k \in V ⟼ (a \in {Base}_{k} ⟼ \{p \in Atoms (k) \| p \leq_{k} a\}))$

Step	Hyp	Ref	Expression
0		cpmap	$class pmap$
1		vk	$setvar k$
2		cvv	$class V$
3		va	$setvar a$
4		cbs	$class Base$
5	1	cv	$setvar k$
6	5 4	cfv	$class {Base}_{k}$
7		vp	$setvar p$
8		catm	$class Atoms$
9	5 8	cfv	$class Atoms (k)$
10	7	cv	$setvar p$
11		cple	$class le$
12	5 11	cfv	$class \leq_{k}$
13	3	cv	$setvar a$
14	10 13 12	wbr	$wff p \leq_{k} a$
15	14 7 9	crab	$class \{p \in Atoms (k) \| p \leq_{k} a\}$
16	3 6 15	cmpt	$class (a \in {Base}_{k} ⟼ \{p \in Atoms (k) \| p \leq_{k} a\})$
17	1 2 16	cmpt	$class (k \in V ⟼ (a \in {Base}_{k} ⟼ \{p \in Atoms (k) \| p \leq_{k} a\}))$
18	0 17	wceq	$wff pmap = (k \in V ⟼ (a \in {Base}_{k} ⟼ \{p \in Atoms (k) \| p \leq_{k} a\}))$

Metamath Proof Explorer