Metamath Proof Explorer

Theorem mapco2g

Description: Renaming indices in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014) (Revised by Mario Carneiro, 5-May-2015)

		Ref	Expression
	Assertion	mapco2g	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to A \circ D \in (B^{E})$

Proof

Step	Hyp	Ref	Expression
1		elmapi	$⊢ A \in (B^{C}) \to A : C ⟶ B$
2		fco	$⊢ (A : C ⟶ B \land D : E ⟶ C) \to (A \circ D) : E ⟶ B$
3	1 2	sylan	$⊢ (A \in (B^{C}) \land D : E ⟶ C) \to (A \circ D) : E ⟶ B$
4	3	3adant1	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to (A \circ D) : E ⟶ B$
5		n0i	$⊢ A \in (B^{C}) \to \neg B^{C} = \emptyset$
6		reldmmap	$⊢ Rel dom ↑_{𝑚}$
7	6	ovprc1	$⊢ \neg B \in V \to B^{C} = \emptyset$
8	5 7	nsyl2	$⊢ A \in (B^{C}) \to B \in V$
9	8	3ad2ant2	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to B \in V$
10		simp1	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to E \in V$
11	9 10	elmapd	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to (A \circ D \in (B^{E}) \leftrightarrow (A \circ D) : E ⟶ B)$
12	4 11	mpbird	$⊢ (E \in V \land A \in (B^{C}) \land D : E ⟶ C) \to A \circ D \in (B^{E})$