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

Metamath Proof Explorer

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 𝐷 ) )