difmap

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

	Ref	Expression
Hypotheses	difmap.a	$⊢ φ \to A \in V$
	difmap.b	$⊢ φ \to B \in W$
	difmap.v	$⊢ φ \to C \in Z$
	difmap.n	$⊢ φ \to C \neq \emptyset$
Assertion	difmap	$⊢ φ \to {(A ∖ B)}^{C} \subseteq (A^{C}) ∖ (B^{C})$

Proof

Step	Hyp	Ref	Expression
1		difmap.a	$⊢ φ \to A \in V$
2		difmap.b	$⊢ φ \to B \in W$
3		difmap.v	$⊢ φ \to C \in Z$
4		difmap.n	$⊢ φ \to C \neq \emptyset$
5		difssd	$⊢ φ \to A ∖ B \subseteq A$
6		mapss	$⊢ (A \in V \land A ∖ B \subseteq A) \to {(A ∖ B)}^{C} \subseteq A^{C}$
7	1 5 6	syl2anc	$⊢ φ \to {(A ∖ B)}^{C} \subseteq A^{C}$
8	7	adantr	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to {(A ∖ B)}^{C} \subseteq A^{C}$
9		simpr	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to f \in ({(A ∖ B)}^{C})$
10	8 9	sseldd	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to f \in (A^{C})$
11		n0	$⊢ C \neq \emptyset \leftrightarrow \exists x x \in C$
12	4 11	sylib	$⊢ φ \to \exists x x \in C$
13	12	adantr	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to \exists x x \in C$
14		simpr	$⊢ (x \in C \land f : C ⟶ B) \to f : C ⟶ B$
15		simpl	$⊢ (x \in C \land f : C ⟶ B) \to x \in C$
16	14 15	ffvelrnd	$⊢ (x \in C \land f : C ⟶ B) \to f (x) \in B$
17	16	adantll	$⊢ (((φ \land f \in ({(A ∖ B)}^{C})) \land x \in C) \land f : C ⟶ B) \to f (x) \in B$
18		elmapi	$⊢ f \in ({(A ∖ B)}^{C}) \to f : C ⟶ A ∖ B$
19	18	adantr	$⊢ (f \in ({(A ∖ B)}^{C}) \land x \in C) \to f : C ⟶ A ∖ B$
20		simpr	$⊢ (f \in ({(A ∖ B)}^{C}) \land x \in C) \to x \in C$
21	19 20	ffvelrnd	$⊢ (f \in ({(A ∖ B)}^{C}) \land x \in C) \to f (x) \in (A ∖ B)$
22		eldifn	$⊢ f (x) \in (A ∖ B) \to \neg f (x) \in B$
23	21 22	syl	$⊢ (f \in ({(A ∖ B)}^{C}) \land x \in C) \to \neg f (x) \in B$
24	23	ad4ant23	$⊢ (((φ \land f \in ({(A ∖ B)}^{C})) \land x \in C) \land f : C ⟶ B) \to \neg f (x) \in B$
25	17 24	pm2.65da	$⊢ ((φ \land f \in ({(A ∖ B)}^{C})) \land x \in C) \to \neg f : C ⟶ B$
26	25	ex	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to (x \in C \to \neg f : C ⟶ B)$
27	26	exlimdv	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to (\exists x x \in C \to \neg f : C ⟶ B)$
28	13 27	mpd	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to \neg f : C ⟶ B$
29		elmapg	$⊢ (B \in W \land C \in Z) \to (f \in (B^{C}) \leftrightarrow f : C ⟶ B)$
30	2 3 29	syl2anc	$⊢ φ \to (f \in (B^{C}) \leftrightarrow f : C ⟶ B)$
31	30	adantr	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to (f \in (B^{C}) \leftrightarrow f : C ⟶ B)$
32	28 31	mtbird	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to \neg f \in (B^{C})$
33	10 32	eldifd	$⊢ (φ \land f \in ({(A ∖ B)}^{C})) \to f \in ((A^{C}) ∖ (B^{C}))$
34	33	ralrimiva	$⊢ φ \to \forall f \in ({(A ∖ B)}^{C}) f \in ((A^{C}) ∖ (B^{C}))$
35		dfss3	$⊢ {(A ∖ B)}^{C} \subseteq (A^{C}) ∖ (B^{C}) \leftrightarrow \forall f \in ({(A ∖ B)}^{C}) f \in ((A^{C}) ∖ (B^{C}))$
36	34 35	sylibr	$⊢ φ \to {(A ∖ B)}^{C} \subseteq (A^{C}) ∖ (B^{C})$

Metamath Proof Explorer

Theorem difmap

Proof