Theorem pmss12g

Description: Subset relation for the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013)

	Ref	Expression
Assertion	pmss12g	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝐴 ↑pm 𝐵 ) ⊆ ( 𝐶 ↑pm 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		xpss12	⊢ ( ( 𝐵 ⊆ 𝐷 ∧ 𝐴 ⊆ 𝐶 ) → ( 𝐵 × 𝐴 ) ⊆ ( 𝐷 × 𝐶 ) )
2	1	ancoms	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) → ( 𝐵 × 𝐴 ) ⊆ ( 𝐷 × 𝐶 ) )
3		sstr	⊢ ( ( 𝑓 ⊆ ( 𝐵 × 𝐴 ) ∧ ( 𝐵 × 𝐴 ) ⊆ ( 𝐷 × 𝐶 ) ) → 𝑓 ⊆ ( 𝐷 × 𝐶 ) )
4	3	expcom	⊢ ( ( 𝐵 × 𝐴 ) ⊆ ( 𝐷 × 𝐶 ) → ( 𝑓 ⊆ ( 𝐵 × 𝐴 ) → 𝑓 ⊆ ( 𝐷 × 𝐶 ) ) )
5	2 4	syl	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) → ( 𝑓 ⊆ ( 𝐵 × 𝐴 ) → 𝑓 ⊆ ( 𝐷 × 𝐶 ) ) )
6	5	anim2d	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) → ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) → ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐷 × 𝐶 ) ) ) )
7	6	adantr	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) → ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐷 × 𝐶 ) ) ) )
8		ssexg	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ 𝑉 ) → 𝐴 ∈ V )
9		ssexg	⊢ ( ( 𝐵 ⊆ 𝐷 ∧ 𝐷 ∈ 𝑊 ) → 𝐵 ∈ V )
10		elpmg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) ) )
11	8 9 10	syl2an	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐵 ⊆ 𝐷 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) ) )
12	11	an4s	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐵 × 𝐴 ) ) ) )
13		elpmg	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( 𝑓 ∈ ( 𝐶 ↑pm 𝐷 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐷 × 𝐶 ) ) ) )
14	13	adantl	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝑓 ∈ ( 𝐶 ↑pm 𝐷 ) ↔ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐷 × 𝐶 ) ) ) )
15	7 12 14	3imtr4d	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝑓 ∈ ( 𝐴 ↑pm 𝐵 ) → 𝑓 ∈ ( 𝐶 ↑pm 𝐷 ) ) )
16	15	ssrdv	⊢ ( ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝐴 ↑pm 𝐵 ) ⊆ ( 𝐶 ↑pm 𝐷 ) )