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 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 )