This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( 𝑘 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpmap ⊢ pmap
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 va ⊢ 𝑎
4 cbs ⊢ Base
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( Base ‘ 𝑘 )
7 vp ⊢ 𝑝
8 catm ⊢ Atoms
9 5 8 cfv ⊢ ( Atoms ‘ 𝑘 )
10 7 cv ⊢ 𝑝
11 cple ⊢ le
12 5 11 cfv ⊢ ( le ‘ 𝑘 )
13 3 cv ⊢ 𝑎
14 10 13 12 wbr ⊢ 𝑝 ( le ‘ 𝑘 ) 𝑎
15 14 7 9 crab ⊢ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 }
16 3 6 15 cmpt ⊢ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } )
17 1 2 16 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } ) )
18 0 17 wceq ⊢ pmap = ( 𝑘 ∈ V ↦ ( 𝑎 ∈ ( Base ‘ 𝑘 ) ↦ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) 𝑎 } ) )