elmapresaun

		Ref	Expression
	Assertion	elmapresaun	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to F \cup G \in (C^{(A \cup B)})$

Step	Hyp	Ref	Expression
1		elmapi	$⊢ F \in (C^{A}) \to F : A ⟶ C$
2		elmapi	$⊢ G \in (C^{B}) \to G : B ⟶ C$
3		id	$⊢ {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)} \to {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}$
4		fresaun	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to (F \cup G) : A \cup B ⟶ C$
5	1 2 3 4	syl3an	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to (F \cup G) : A \cup B ⟶ C$
6		elmapex	$⊢ F \in (C^{A}) \to (C \in V \land A \in V)$
7	6	simpld	$⊢ F \in (C^{A}) \to C \in V$
8	7	3ad2ant1	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to C \in V$
9	6	simprd	$⊢ F \in (C^{A}) \to A \in V$
10		elmapex	$⊢ G \in (C^{B}) \to (C \in V \land B \in V)$
11	10	simprd	$⊢ G \in (C^{B}) \to B \in V$
12		unexg	$⊢ (A \in V \land B \in V) \to A \cup B \in V$
13	9 11 12	syl2an	$⊢ (F \in (C^{A}) \land G \in (C^{B})) \to A \cup B \in V$
14	13	3adant3	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to A \cup B \in V$
15	8 14	elmapd	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to (F \cup G \in (C^{(A \cup B)}) \leftrightarrow (F \cup G) : A \cup B ⟶ C)$
16	5 15	mpbird	$⊢ (F \in (C^{A}) \land G \in (C^{B}) \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to F \cup G \in (C^{(A \cup B)})$

Metamath Proof Explorer