suppssfv

Description: Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 28-May-2019)

	Ref	Expression
Hypotheses	suppssfv.a	$⊢ φ \to (x \in D ⟼ A) supp Y \subseteq L$
	suppssfv.f	$⊢ φ \to F (Y) = Z$
	suppssfv.v	$⊢ (φ \land x \in D) \to A \in V$
	suppssfv.y	$⊢ φ \to Y \in U$
Assertion	suppssfv	$⊢ φ \to (x \in D ⟼ F (A)) supp Z \subseteq L$

Proof

Step	Hyp	Ref	Expression
1		suppssfv.a	$⊢ φ \to (x \in D ⟼ A) supp Y \subseteq L$
2		suppssfv.f	$⊢ φ \to F (Y) = Z$
3		suppssfv.v	$⊢ (φ \land x \in D) \to A \in V$
4		suppssfv.y	$⊢ φ \to Y \in U$
5		eldifsni	$⊢ F (A) \in (V ∖ \{Z\}) \to F (A) \neq Z$
6	3	elexd	$⊢ (φ \land x \in D) \to A \in V$
7	6	ad4ant23	$⊢ ((((D \in V \land Z \in V) \land φ) \land x \in D) \land F (A) \neq Z) \to A \in V$
8		fveqeq2	$⊢ A = Y \to (F (A) = Z \leftrightarrow F (Y) = Z)$
9	2 8	syl5ibrcom	$⊢ φ \to (A = Y \to F (A) = Z)$
10	9	necon3d	$⊢ φ \to (F (A) \neq Z \to A \neq Y)$
11	10	ad2antlr	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to (F (A) \neq Z \to A \neq Y)$
12	11	imp	$⊢ ((((D \in V \land Z \in V) \land φ) \land x \in D) \land F (A) \neq Z) \to A \neq Y$
13		eldifsn	$⊢ A \in (V ∖ \{Y\}) \leftrightarrow (A \in V \land A \neq Y)$
14	7 12 13	sylanbrc	$⊢ ((((D \in V \land Z \in V) \land φ) \land x \in D) \land F (A) \neq Z) \to A \in (V ∖ \{Y\})$
15	14	ex	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to (F (A) \neq Z \to A \in (V ∖ \{Y\}))$
16	5 15	syl5	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to (F (A) \in (V ∖ \{Z\}) \to A \in (V ∖ \{Y\}))$
17	16	ss2rabdv	$⊢ ((D \in V \land Z \in V) \land φ) \to \{x \in D \| F (A) \in (V ∖ \{Z\})\} \subseteq \{x \in D \| A \in (V ∖ \{Y\})\}$
18		eqid	$⊢ (x \in D ⟼ F (A)) = (x \in D ⟼ F (A))$
19		simpll	$⊢ ((D \in V \land Z \in V) \land φ) \to D \in V$
20		simplr	$⊢ ((D \in V \land Z \in V) \land φ) \to Z \in V$
21	18 19 20	mptsuppdifd	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ F (A)) supp Z = \{x \in D \| F (A) \in (V ∖ \{Z\})\}$
22		eqid	$⊢ (x \in D ⟼ A) = (x \in D ⟼ A)$
23	4	adantl	$⊢ ((D \in V \land Z \in V) \land φ) \to Y \in U$
24	22 19 23	mptsuppdifd	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A) supp Y = \{x \in D \| A \in (V ∖ \{Y\})\}$
25	17 21 24	3sstr4d	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ F (A)) supp Z \subseteq (x \in D ⟼ A) supp Y$
26	1	adantl	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A) supp Y \subseteq L$
27	25 26	sstrd	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ F (A)) supp Z \subseteq L$
28	27	ex	$⊢ (D \in V \land Z \in V) \to (φ \to (x \in D ⟼ F (A)) supp Z \subseteq L)$
29		mptexg	$⊢ D \in V \to (x \in D ⟼ F (A)) \in V$
30		fvex	$⊢ F (A) \in V$
31	30	rgenw	$⊢ \forall x \in D F (A) \in V$
32		dmmptg	$⊢ \forall x \in D F (A) \in V \to dom (x \in D ⟼ F (A)) = D$
33	31 32	ax-mp	$⊢ dom (x \in D ⟼ F (A)) = D$
34		dmexg	$⊢ (x \in D ⟼ F (A)) \in V \to dom (x \in D ⟼ F (A)) \in V$
35	33 34	eqeltrrid	$⊢ (x \in D ⟼ F (A)) \in V \to D \in V$
36	29 35	impbii	$⊢ D \in V \leftrightarrow (x \in D ⟼ F (A)) \in V$
37	36	anbi1i	$⊢ (D \in V \land Z \in V) \leftrightarrow ((x \in D ⟼ F (A)) \in V \land Z \in V)$
38		supp0prc	$⊢ \neg ((x \in D ⟼ F (A)) \in V \land Z \in V) \to (x \in D ⟼ F (A)) supp Z = \emptyset$
39	37 38	sylnbi	$⊢ \neg (D \in V \land Z \in V) \to (x \in D ⟼ F (A)) supp Z = \emptyset$
40		0ss	$⊢ \emptyset \subseteq L$
41	39 40	eqsstrdi	$⊢ \neg (D \in V \land Z \in V) \to (x \in D ⟼ F (A)) supp Z \subseteq L$
42	41	a1d	$⊢ \neg (D \in V \land Z \in V) \to (φ \to (x \in D ⟼ F (A)) supp Z \subseteq L)$
43	28 42	pm2.61i	$⊢ φ \to (x \in D ⟼ F (A)) supp Z \subseteq L$

Metamath Proof Explorer

Theorem suppssfv

Proof