elmapssres

Description: A restricted mapping is a mapping. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Mario Carneiro, 5-May-2015)

		Ref	Expression
	Assertion	elmapssres	$⊢ (A \in (B^{C}) \land D \subseteq C) \to {A ↾}_{D} \in (B^{D})$

Step	Hyp	Ref	Expression
1		elmapi	$⊢ A \in (B^{C}) \to A : C ⟶ B$
2		fssres	$⊢ (A : C ⟶ B \land D \subseteq C) \to ({A ↾}_{D}) : D ⟶ B$
3	1 2	sylan	$⊢ (A \in (B^{C}) \land D \subseteq C) \to ({A ↾}_{D}) : D ⟶ B$
4		elmapex	$⊢ A \in (B^{C}) \to (B \in V \land C \in V)$
5	4	simpld	$⊢ A \in (B^{C}) \to B \in V$
6	5	adantr	$⊢ (A \in (B^{C}) \land D \subseteq C) \to B \in V$
7	4	simprd	$⊢ A \in (B^{C}) \to C \in V$
8		ssexg	$⊢ (D \subseteq C \land C \in V) \to D \in V$
9	8	ancoms	$⊢ (C \in V \land D \subseteq C) \to D \in V$
10	7 9	sylan	$⊢ (A \in (B^{C}) \land D \subseteq C) \to D \in V$
11	6 10	elmapd	$⊢ (A \in (B^{C}) \land D \subseteq C) \to ({A ↾}_{D} \in (B^{D}) \leftrightarrow ({A ↾}_{D}) : D ⟶ B)$
12	3 11	mpbird	$⊢ (A \in (B^{C}) \land D \subseteq C) \to {A ↾}_{D} \in (B^{D})$

Metamath Proof Explorer