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

Metamath Proof Explorer

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 𝑓 } )