Definition df-pm

Description: Define the partial mapping operation. A partial function from B to A is a function from a subset of B to A . The set of all partial functions from B to A is written ( A ^pm B ) (see pmvalg ). A notation for this operation apparently does not appear in the literature. We use ^pm to distinguish it from the less general set exponentiation operation ^m ( df-map ). See mapsspm for its relationship to set exponentiation. (Contributed by NM, 15-Nov-2007)

	Ref	Expression
Assertion	df-pm	⊢ ↑pm = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∈ 𝒫 ( 𝑦 × 𝑥 ) ∣ Fun 𝑓 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpm	⊢ ↑pm
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4		vf	⊢ 𝑓
5	3	cv	⊢ 𝑦
6	1	cv	⊢ 𝑥
7	5 6	cxp	⊢ ( 𝑦 × 𝑥 )
8	7	cpw	⊢ 𝒫 ( 𝑦 × 𝑥 )
9	4	cv	⊢ 𝑓
10	9	wfun	⊢ Fun 𝑓
11	10 4 8	crab	⊢ { 𝑓 ∈ 𝒫 ( 𝑦 × 𝑥 ) ∣ Fun 𝑓 }
12	1 3 2 2 11	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∈ 𝒫 ( 𝑦 × 𝑥 ) ∣ Fun 𝑓 } )
13	0 12	wceq	⊢ ↑pm = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∈ 𝒫 ( 𝑦 × 𝑥 ) ∣ Fun 𝑓 } )