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	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \in V \land D \in W)) \to A ↑_{𝑝𝑚} B \subseteq C ↑_{𝑝𝑚} D$

Proof

Step	Hyp	Ref	Expression
1		xpss12	$⊢ (B \subseteq D \land A \subseteq C) \to B \times A \subseteq D \times C$
2	1	ancoms	$⊢ (A \subseteq C \land B \subseteq D) \to B \times A \subseteq D \times C$
3		sstr	$⊢ (f \subseteq B \times A \land B \times A \subseteq D \times C) \to f \subseteq D \times C$
4	3	expcom	$⊢ B \times A \subseteq D \times C \to (f \subseteq B \times A \to f \subseteq D \times C)$
5	2 4	syl	$⊢ (A \subseteq C \land B \subseteq D) \to (f \subseteq B \times A \to f \subseteq D \times C)$
6	5	anim2d	$⊢ (A \subseteq C \land B \subseteq D) \to ((Fun f \land f \subseteq B \times A) \to (Fun f \land f \subseteq D \times C))$
7	6	adantr	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \in V \land D \in W)) \to ((Fun f \land f \subseteq B \times A) \to (Fun f \land f \subseteq D \times C))$
8		ssexg	$⊢ (A \subseteq C \land C \in V) \to A \in V$
9		ssexg	$⊢ (B \subseteq D \land D \in W) \to B \in V$
10		elpmg	$⊢ (A \in V \land B \in V) \to (f \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun f \land f \subseteq B \times A))$
11	8 9 10	syl2an	$⊢ ((A \subseteq C \land C \in V) \land (B \subseteq D \land D \in W)) \to (f \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun f \land f \subseteq B \times A))$
12	11	an4s	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \in V \land D \in W)) \to (f \in (A ↑_{𝑝𝑚} B) \leftrightarrow (Fun f \land f \subseteq B \times A))$
13		elpmg	$⊢ (C \in V \land D \in W) \to (f \in (C ↑_{𝑝𝑚} D) \leftrightarrow (Fun f \land f \subseteq D \times C))$
14	13	adantl	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \in V \land D \in W)) \to (f \in (C ↑_{𝑝𝑚} D) \leftrightarrow (Fun f \land f \subseteq D \times C))$
15	7 12 14	3imtr4d	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \in V \land D \in W)) \to (f \in (A ↑_{𝑝𝑚} B) \to f \in (C ↑_{𝑝𝑚} D))$
16	15	ssrdv	$⊢ ((A \subseteq C \land B \subseteq D) \land (C \in V \land D \in W)) \to A ↑_{𝑝𝑚} B \subseteq C ↑_{𝑝𝑚} D$