mapssbi

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

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

Proof

Step	Hyp	Ref	Expression
1		mapssbi.a	$⊢ φ \to A \in V$
2		mapssbi.b	$⊢ φ \to B \in W$
3		mapssbi.c	$⊢ φ \to C \in Z$
4		mapssbi.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		simplr	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land \neg A \subseteq B) \to A^{C} \subseteq B^{C}$
11		nssrex	$⊢ \neg A \subseteq B \leftrightarrow \exists x \in A \neg x \in B$
12	11	bilani	$⊢ (φ \land \neg A \subseteq B) \to \exists x \in A \neg x \in B$
13		fconst6g	$⊢ x \in A \to (C \times \{x\}) : C ⟶ A$
14	13	adantl	$⊢ (φ \land x \in A) \to (C \times \{x\}) : C ⟶ A$
15		elmapg	$⊢ (A \in V \land C \in Z) \to (C \times \{x\} \in (A^{C}) \leftrightarrow (C \times \{x\}) : C ⟶ A)$
16	1 3 15	syl2anc	$⊢ φ \to (C \times \{x\} \in (A^{C}) \leftrightarrow (C \times \{x\}) : C ⟶ A)$
17	16	adantr	$⊢ (φ \land x \in A) \to (C \times \{x\} \in (A^{C}) \leftrightarrow (C \times \{x\}) : C ⟶ A)$
18	14 17	mpbird	$⊢ (φ \land x \in A) \to C \times \{x\} \in (A^{C})$
19	18	3adant3	$⊢ (φ \land x \in A \land \neg x \in B) \to C \times \{x\} \in (A^{C})$
20	3	adantr	$⊢ (φ \land C \times \{x\} \in (B^{C})) \to C \in Z$
21	2	adantr	$⊢ (φ \land C \times \{x\} \in (B^{C})) \to B \in W$
22	4	adantr	$⊢ (φ \land C \times \{x\} \in (B^{C})) \to C \neq \emptyset$
23		simpr	$⊢ (φ \land C \times \{x\} \in (B^{C})) \to C \times \{x\} \in (B^{C})$
24	20 21 22 23	snelmap	$⊢ (φ \land C \times \{x\} \in (B^{C})) \to x \in B$
25	24	adantlr	$⊢ ((φ \land \neg x \in B) \land C \times \{x\} \in (B^{C})) \to x \in B$
26		simplr	$⊢ ((φ \land \neg x \in B) \land C \times \{x\} \in (B^{C})) \to \neg x \in B$
27	25 26	pm2.65da	$⊢ (φ \land \neg x \in B) \to \neg C \times \{x\} \in (B^{C})$
28	27	3adant2	$⊢ (φ \land x \in A \land \neg x \in B) \to \neg C \times \{x\} \in (B^{C})$
29		nelss	$⊢ (C \times \{x\} \in (A^{C}) \land \neg C \times \{x\} \in (B^{C})) \to \neg A^{C} \subseteq B^{C}$
30	19 28 29	syl2anc	$⊢ (φ \land x \in A \land \neg x \in B) \to \neg A^{C} \subseteq B^{C}$
31	30	3exp	$⊢ φ \to (x \in A \to (\neg x \in B \to \neg A^{C} \subseteq B^{C}))$
32	31	adantr	$⊢ (φ \land \neg A \subseteq B) \to (x \in A \to (\neg x \in B \to \neg A^{C} \subseteq B^{C}))$
33	32	rexlimdv	$⊢ (φ \land \neg A \subseteq B) \to (\exists x \in A \neg x \in B \to \neg A^{C} \subseteq B^{C})$
34	12 33	mpd	$⊢ (φ \land \neg A \subseteq B) \to \neg A^{C} \subseteq B^{C}$
35	34	adantlr	$⊢ ((φ \land A^{C} \subseteq B^{C}) \land \neg A \subseteq B) \to \neg A^{C} \subseteq B^{C}$
36	10 35	condan	$⊢ (φ \land A^{C} \subseteq B^{C}) \to A \subseteq B$
37	36	ex	$⊢ φ \to (A^{C} \subseteq B^{C} \to A \subseteq B)$
38	9 37	impbid	$⊢ φ \to (A \subseteq B \leftrightarrow A^{C} \subseteq B^{C})$

Metamath Proof Explorer

Theorem mapssbi

Proof