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

Metamath Proof Explorer

Theorem pmsspw

Description: Partial maps are a subset of the power set of the Cartesian product of its arguments. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion pmsspw ( 𝐴 ↑pm 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 )

Proof

Step Hyp Ref Expression
1 n0i ⊢ ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → ¬ ( 𝐴 ↑pm 𝐵 ) = ∅ )
2 fnpm ⊢ ↑pm Fn ( V × V )
3 2 fndmi ⊢ dom ↑pm = ( V × V )
4 3 ndmov ⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ↑pm 𝐵 ) = ∅ )
5 1 4 nsyl2 ⊢ ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
6 elpmg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) ) )
7 5 6 syl ⊢ ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) ) )
8 7 ibi ⊢ ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) )
9 8 simprd ⊢ ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → 𝑓 ⊆ ( 𝐵 × 𝐴 ) )
10 velpw ⊢ ( 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) ↔ 𝑓 ⊆ ( 𝐵 × 𝐴 ) )
11 9 10 sylibr ⊢ ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → 𝑓 ∈ 𝒫 ( 𝐵 × 𝐴 ) )
12 11 ssriv ⊢ ( 𝐴 ↑pm 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 )