Metamath Proof Explorer

Definition 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 ∈ V ⟼ a ∈ Base k ⟼ p ∈ Atoms ⁡ k | p ≤ k a

Detailed syntax breakdown

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 ≤ k
13 3 cv setvar a
14 10 13 12 wbr wff p ≤ k a
15 14 7 9 crab class p ∈ Atoms ⁡ k | p ≤ k a
16 3 6 15 cmpt class a ∈ Base k ⟼ p ∈ Atoms ⁡ k | p ≤ k a
17 1 2 16 cmpt class k ∈ V ⟼ a ∈ Base k ⟼ p ∈ Atoms ⁡ k | p ≤ k a
18 0 17 wceq wff pmap = k ∈ V ⟼ a ∈ Base k ⟼ p ∈ Atoms ⁡ k | p ≤ k a