Theorem pmvalg

Description: The value of the partial mapping operation. ( A ^pm B ) is the set of all partial functions that map from B to A . (Contributed by NM, 15-Nov-2007) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	pmvalg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ↑pm 𝐵 ) = { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } )

Proof

Step	Hyp	Ref	Expression
1		ssrab2	⊢ { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ⊆ 𝒫 ( 𝐵 × 𝐴 )
2		xpexg	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐵 × 𝐴 ) ∈ V )
3	2	ancoms	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐵 × 𝐴 ) ∈ V )
4	3	pwexd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝒫 ( 𝐵 × 𝐴 ) ∈ V )
5		ssexg	⊢ ( ( { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ⊆ 𝒫 ( 𝐵 × 𝐴 ) ∧ 𝒫 ( 𝐵 × 𝐴 ) ∈ V ) → { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ∈ V )
6	1 4 5	sylancr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ∈ V )
7		elex	⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
8		elex	⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V )
9		xpeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 × 𝑥 ) = ( 𝑦 × 𝐴 ) )
10	9	pweqd	⊢ ( 𝑥 = 𝐴 → 𝒫 ( 𝑦 × 𝑥 ) = 𝒫 ( 𝑦 × 𝐴 ) )
11	10	rabeqdv	⊢ ( 𝑥 = 𝐴 → { 𝑓 ∈ 𝒫 ( 𝑦 × 𝑥 ) ∣ Fun 𝑓 } = { 𝑓 ∈ 𝒫 ( 𝑦 × 𝐴 ) ∣ Fun 𝑓 } )
12		xpeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 × 𝐴 ) = ( 𝐵 × 𝐴 ) )
13	12	pweqd	⊢ ( 𝑦 = 𝐵 → 𝒫 ( 𝑦 × 𝐴 ) = 𝒫 ( 𝐵 × 𝐴 ) )
14	13	rabeqdv	⊢ ( 𝑦 = 𝐵 → { 𝑓 ∈ 𝒫 ( 𝑦 × 𝐴 ) ∣ Fun 𝑓 } = { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } )
15		df-pm	⊢ ↑pm = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∈ 𝒫 ( 𝑦 × 𝑥 ) ∣ Fun 𝑓 } )
16	11 14 15	ovmpog	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ∈ V ) → ( 𝐴 ↑pm 𝐵 ) = { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } )
17	16	3expia	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ∈ V → ( 𝐴 ↑pm 𝐵 ) = { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ) )
18	7 8 17	syl2an	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ∈ V → ( 𝐴 ↑pm 𝐵 ) = { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } ) )
19	6 18	mpd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ↑pm 𝐵 ) = { 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∣ Fun 𝑓 } )