mapss2

Description: Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		mapss2.a	$⊢ φ \to A \in V$
2		mapss2.b	$⊢ φ \to B \in W$
3		mapss2.c	$⊢ φ \to C \in Z$
4		mapss2.n	$⊢ φ \to C \neq \emptyset$
5	2	adantr	$⊢ (φ \land A \subseteq B) \to B \in W$
6		simpr	$⊢ (φ \land A \subseteq B) \to A \subseteq B$
7		mapss	$⊢ (B \in W \land A \subseteq B) \to A^{C} \subseteq B^{C}$
8	5 6 7	syl2anc	$⊢ (φ \land A \subseteq B) \to A^{C} \subseteq B^{C}$
9	8	ex	$⊢ φ \to (A \subseteq B \to A^{C} \subseteq B^{C})$
10		n0	$⊢ C \neq \emptyset \leftrightarrow \exists x x \in C$
11	4 10	sylib	$⊢ φ \to \exists x x \in C$
12	11	adantr	$⊢ (φ \land A^{C} \subseteq B^{C}) \to \exists x x \in C$
13		eqidd	$⊢ (φ \land x \in C) \to (w \in C ⟼ y) = (w \in C ⟼ y)$
14		eqidd	$⊢ ((φ \land x \in C) \land w = x) \to y = y$
15		simpr	$⊢ (φ \land x \in C) \to x \in C$
16		vex	$⊢ y \in V$
17	16	a1i	$⊢ (φ \land x \in C) \to y \in V$
18	13 14 15 17	fvmptd	$⊢ (φ \land x \in C) \to (w \in C ⟼ y) (x) = y$
19	18	eqcomd	$⊢ (φ \land x \in C) \to y = (w \in C ⟼ y) (x)$
20	19	ad4ant13	$⊢ (((φ \land A^{C} \subseteq B^{C}) \land x \in C) \land y \in A) \to y = (w \in C ⟼ y) (x)$
21		simplr	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land y \in A) \to A^{C} \subseteq B^{C}$
22		simplr	$⊢ ((φ \land y \in A) \land w \in C) \to y \in A$
23	22	fmpttd	$⊢ (φ \land y \in A) \to (w \in C ⟼ y) : C ⟶ A$
24	1	adantr	$⊢ (φ \land y \in A) \to A \in V$
25	3	adantr	$⊢ (φ \land y \in A) \to C \in Z$
26	24 25	elmapd	$⊢ (φ \land y \in A) \to ((w \in C ⟼ y) \in (A^{C}) \leftrightarrow (w \in C ⟼ y) : C ⟶ A)$
27	23 26	mpbird	$⊢ (φ \land y \in A) \to (w \in C ⟼ y) \in (A^{C})$
28	27	adantlr	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land y \in A) \to (w \in C ⟼ y) \in (A^{C})$
29	21 28	sseldd	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land y \in A) \to (w \in C ⟼ y) \in (B^{C})$
30		elmapi	$⊢ (w \in C ⟼ y) \in (B^{C}) \to (w \in C ⟼ y) : C ⟶ B$
31	29 30	syl	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land y \in A) \to (w \in C ⟼ y) : C ⟶ B$
32	31	adantlr	$⊢ (((φ \land A^{C} \subseteq B^{C}) \land x \in C) \land y \in A) \to (w \in C ⟼ y) : C ⟶ B$
33		simplr	$⊢ (((φ \land A^{C} \subseteq B^{C}) \land x \in C) \land y \in A) \to x \in C$
34	32 33	ffvelrnd	$⊢ (((φ \land A^{C} \subseteq B^{C}) \land x \in C) \land y \in A) \to (w \in C ⟼ y) (x) \in B$
35	20 34	eqeltrd	$⊢ (((φ \land A^{C} \subseteq B^{C}) \land x \in C) \land y \in A) \to y \in B$
36	35	ralrimiva	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land x \in C) \to \forall y \in A y \in B$
37		dfss3	$⊢ A \subseteq B \leftrightarrow \forall y \in A y \in B$
38	36 37	sylibr	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land x \in C) \to A \subseteq B$
39	38	ex	$⊢ (φ \land A^{C} \subseteq B^{C}) \to (x \in C \to A \subseteq B)$
40	39	exlimdv	$⊢ (φ \land A^{C} \subseteq B^{C}) \to (\exists x x \in C \to A \subseteq B)$
41	12 40	mpd	$⊢ (φ \land A^{C} \subseteq B^{C}) \to A \subseteq B$
42	41	ex	$⊢ φ \to (A^{C} \subseteq B^{C} \to A \subseteq B)$
43	9 42	impbid	$⊢ φ \to (A \subseteq B \leftrightarrow A^{C} \subseteq B^{C})$

Metamath Proof Explorer

Theorem mapss2

Proof