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

Metamath Proof Explorer

Theorem mapssbi

Proof