inmap

Description: Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	inmap.a	$⊢ φ \to A \in V$
	inmap.b	$⊢ φ \to B \in W$
	inmap.c	$⊢ φ \to C \in Z$
Assertion	inmap	$⊢ φ \to (A^{C}) \cap (B^{C}) = {(A \cap B)}^{C}$

Proof

Step	Hyp	Ref	Expression
1		inmap.a	$⊢ φ \to A \in V$
2		inmap.b	$⊢ φ \to B \in W$
3		inmap.c	$⊢ φ \to C \in Z$
4		elinel1	$⊢ f \in ((A^{C}) \cap (B^{C})) \to f \in (A^{C})$
5		elmapi	$⊢ f \in (A^{C}) \to f : C ⟶ A$
6	4 5	syl	$⊢ f \in ((A^{C}) \cap (B^{C})) \to f : C ⟶ A$
7		elinel2	$⊢ f \in ((A^{C}) \cap (B^{C})) \to f \in (B^{C})$
8		elmapi	$⊢ f \in (B^{C}) \to f : C ⟶ B$
9	7 8	syl	$⊢ f \in ((A^{C}) \cap (B^{C})) \to f : C ⟶ B$
10	6 9	jca	$⊢ f \in ((A^{C}) \cap (B^{C})) \to (f : C ⟶ A \land f : C ⟶ B)$
11		fin	$⊢ f : C ⟶ A \cap B \leftrightarrow (f : C ⟶ A \land f : C ⟶ B)$
12	10 11	sylibr	$⊢ f \in ((A^{C}) \cap (B^{C})) \to f : C ⟶ A \cap B$
13	12	adantl	$⊢ (φ \land f \in ((A^{C}) \cap (B^{C}))) \to f : C ⟶ A \cap B$
14		inss1	$⊢ A \cap B \subseteq A$
15	14	a1i	$⊢ φ \to A \cap B \subseteq A$
16	1 15	ssexd	$⊢ φ \to A \cap B \in V$
17	16 3	elmapd	$⊢ φ \to (f \in ({(A \cap B)}^{C}) \leftrightarrow f : C ⟶ A \cap B)$
18	17	adantr	$⊢ (φ \land f \in ((A^{C}) \cap (B^{C}))) \to (f \in ({(A \cap B)}^{C}) \leftrightarrow f : C ⟶ A \cap B)$
19	13 18	mpbird	$⊢ (φ \land f \in ((A^{C}) \cap (B^{C}))) \to f \in ({(A \cap B)}^{C})$
20	19	ralrimiva	$⊢ φ \to \forall f \in ((A^{C}) \cap (B^{C})) f \in ({(A \cap B)}^{C})$
21		dfss3	$⊢ (A^{C}) \cap (B^{C}) \subseteq {(A \cap B)}^{C} \leftrightarrow \forall f \in ((A^{C}) \cap (B^{C})) f \in ({(A \cap B)}^{C})$
22	20 21	sylibr	$⊢ φ \to (A^{C}) \cap (B^{C}) \subseteq {(A \cap B)}^{C}$
23		mapss	$⊢ (A \in V \land A \cap B \subseteq A) \to {(A \cap B)}^{C} \subseteq A^{C}$
24	1 15 23	syl2anc	$⊢ φ \to {(A \cap B)}^{C} \subseteq A^{C}$
25		inss2	$⊢ A \cap B \subseteq B$
26	25	a1i	$⊢ φ \to A \cap B \subseteq B$
27		mapss	$⊢ (B \in W \land A \cap B \subseteq B) \to {(A \cap B)}^{C} \subseteq B^{C}$
28	2 26 27	syl2anc	$⊢ φ \to {(A \cap B)}^{C} \subseteq B^{C}$
29	24 28	ssind	$⊢ φ \to {(A \cap B)}^{C} \subseteq (A^{C}) \cap (B^{C})$
30	22 29	eqssd	$⊢ φ \to (A^{C}) \cap (B^{C}) = {(A \cap B)}^{C}$

Metamath Proof Explorer

Theorem inmap

Proof