suppss3

Description: Deduce a function's support's inclusion in another function's support. (Contributed by Thierry Arnoux, 7-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	suppss3.1	$⊢ G = (x \in A ⟼ B)$
	suppss3.a	$⊢ φ \to A \in V$
	suppss3.z	$⊢ φ \to Z \in W$
	suppss3.2	$⊢ φ \to F Fn A$
	suppss3.3	$⊢ (φ \land x \in A \land F (x) = Z) \to B = Z$
Assertion	suppss3	$⊢ φ \to G supp Z \subseteq F supp Z$

Proof

Step	Hyp	Ref	Expression
1		suppss3.1	$⊢ G = (x \in A ⟼ B)$
2		suppss3.a	$⊢ φ \to A \in V$
3		suppss3.z	$⊢ φ \to Z \in W$
4		suppss3.2	$⊢ φ \to F Fn A$
5		suppss3.3	$⊢ (φ \land x \in A \land F (x) = Z) \to B = Z$
6	1	oveq1i	$⊢ G supp Z = (x \in A ⟼ B) supp Z$
7		simpl	$⊢ (φ \land x \in (A ∖ {supp}_{Z} (F))) \to φ$
8		eldifi	$⊢ x \in (A ∖ {supp}_{Z} (F)) \to x \in A$
9	8	adantl	$⊢ (φ \land x \in (A ∖ {supp}_{Z} (F))) \to x \in A$
10		fnex	$⊢ (F Fn A \land A \in V) \to F \in V$
11	4 2 10	syl2anc	$⊢ φ \to F \in V$
12		suppimacnv	$⊢ (F \in V \land Z \in W) \to F supp Z = F^{-1} [V ∖ \{Z\}]$
13	11 3 12	syl2anc	$⊢ φ \to F supp Z = F^{-1} [V ∖ \{Z\}]$
14	13	eleq2d	$⊢ φ \to (x \in {supp}_{Z} (F) \leftrightarrow x \in F^{-1} [V ∖ \{Z\}])$
15		elpreima	$⊢ F Fn A \to (x \in F^{-1} [V ∖ \{Z\}] \leftrightarrow (x \in A \land F (x) \in (V ∖ \{Z\})))$
16	4 15	syl	$⊢ φ \to (x \in F^{-1} [V ∖ \{Z\}] \leftrightarrow (x \in A \land F (x) \in (V ∖ \{Z\})))$
17	14 16	bitrd	$⊢ φ \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in A \land F (x) \in (V ∖ \{Z\})))$
18	17	baibd	$⊢ (φ \land x \in A) \to (x \in {supp}_{Z} (F) \leftrightarrow F (x) \in (V ∖ \{Z\}))$
19	18	notbid	$⊢ (φ \land x \in A) \to (\neg x \in {supp}_{Z} (F) \leftrightarrow \neg F (x) \in (V ∖ \{Z\}))$
20	19	biimpd	$⊢ (φ \land x \in A) \to (\neg x \in {supp}_{Z} (F) \to \neg F (x) \in (V ∖ \{Z\}))$
21	20	expimpd	$⊢ φ \to ((x \in A \land \neg x \in {supp}_{Z} (F)) \to \neg F (x) \in (V ∖ \{Z\}))$
22		eldif	$⊢ x \in (A ∖ {supp}_{Z} (F)) \leftrightarrow (x \in A \land \neg x \in {supp}_{Z} (F))$
23		fvex	$⊢ F (x) \in V$
24		eldifsn	$⊢ F (x) \in (V ∖ \{Z\}) \leftrightarrow (F (x) \in V \land F (x) \neq Z)$
25	23 24	mpbiran	$⊢ F (x) \in (V ∖ \{Z\}) \leftrightarrow F (x) \neq Z$
26	25	necon2bbii	$⊢ F (x) = Z \leftrightarrow \neg F (x) \in (V ∖ \{Z\})$
27	21 22 26	3imtr4g	$⊢ φ \to (x \in (A ∖ {supp}_{Z} (F)) \to F (x) = Z)$
28	27	imp	$⊢ (φ \land x \in (A ∖ {supp}_{Z} (F))) \to F (x) = Z$
29	7 9 28 5	syl3anc	$⊢ (φ \land x \in (A ∖ {supp}_{Z} (F))) \to B = Z$
30	29 2	suppss2	$⊢ φ \to (x \in A ⟼ B) supp Z \subseteq F supp Z$
31	6 30	eqsstrid	$⊢ φ \to G supp Z \subseteq F supp Z$

Metamath Proof Explorer

Theorem suppss3

Proof