suppss2f

Description: Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017) (Revised by AV, 1-Sep-2020)

	Ref	Expression
Hypotheses	suppss2f.p	$⊢ Ⅎ k φ$
	suppss2f.a	$⊢ \underline{Ⅎ} k A$
	suppss2f.w	$⊢ \underline{Ⅎ} k W$
	suppss2f.n	$⊢ (φ \land k \in (A ∖ W)) \to B = Z$
	suppss2f.v	$⊢ φ \to A \in V$
Assertion	suppss2f	$⊢ φ \to (k \in A ⟼ B) supp Z \subseteq W$

Proof

Step	Hyp	Ref	Expression
1		suppss2f.p	$⊢ Ⅎ k φ$
2		suppss2f.a	$⊢ \underline{Ⅎ} k A$
3		suppss2f.w	$⊢ \underline{Ⅎ} k W$
4		suppss2f.n	$⊢ (φ \land k \in (A ∖ W)) \to B = Z$
5		suppss2f.v	$⊢ φ \to A \in V$
6		nfcv	$⊢ \underline{Ⅎ} l A$
7		nfcv	$⊢ \underline{Ⅎ} l B$
8		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ l / k ⦌ B$
9		csbeq1a	$⊢ k = l \to B = ⦋ l / k ⦌ B$
10	2 6 7 8 9	cbvmptf	$⊢ (k \in A ⟼ B) = (l \in A ⟼ ⦋ l / k ⦌ B)$
11	10	oveq1i	$⊢ (k \in A ⟼ B) supp Z = (l \in A ⟼ ⦋ l / k ⦌ B) supp Z$
12	4	sbt	$⊢ [l/ k] ((φ \land k \in (A ∖ W)) \to B = Z)$
13		sbim	$⊢ [l/ k] ((φ \land k \in (A ∖ W)) \to B = Z) \leftrightarrow ([l/ k] (φ \land k \in (A ∖ W)) \to [l/ k] B = Z)$
14		sban	$⊢ [l/ k] (φ \land k \in (A ∖ W)) \leftrightarrow ([l/ k] φ \land [l/ k] k \in (A ∖ W))$
15	1	sbf	$⊢ [l/ k] φ \leftrightarrow φ$
16	2 3	nfdif	$⊢ \underline{Ⅎ} k (A ∖ W)$
17	16	clelsb1fw	$⊢ [l/ k] k \in (A ∖ W) \leftrightarrow l \in (A ∖ W)$
18	15 17	anbi12i	$⊢ ([l/ k] φ \land [l/ k] k \in (A ∖ W)) \leftrightarrow (φ \land l \in (A ∖ W))$
19	14 18	bitri	$⊢ [l/ k] (φ \land k \in (A ∖ W)) \leftrightarrow (φ \land l \in (A ∖ W))$
20		sbsbc	$⊢ [l/ k] B = Z \leftrightarrow \underset{˙}{[} l / k \underset{˙}{]} B = Z$
21		sbceq1g	$⊢ l \in V \to (\underset{˙}{[} l / k \underset{˙}{]} B = Z \leftrightarrow ⦋ l / k ⦌ B = Z)$
22	21	elv	$⊢ \underset{˙}{[} l / k \underset{˙}{]} B = Z \leftrightarrow ⦋ l / k ⦌ B = Z$
23	20 22	bitri	$⊢ [l/ k] B = Z \leftrightarrow ⦋ l / k ⦌ B = Z$
24	19 23	imbi12i	$⊢ ([l/ k] (φ \land k \in (A ∖ W)) \to [l/ k] B = Z) \leftrightarrow ((φ \land l \in (A ∖ W)) \to ⦋ l / k ⦌ B = Z)$
25	13 24	bitri	$⊢ [l/ k] ((φ \land k \in (A ∖ W)) \to B = Z) \leftrightarrow ((φ \land l \in (A ∖ W)) \to ⦋ l / k ⦌ B = Z)$
26	12 25	mpbi	$⊢ (φ \land l \in (A ∖ W)) \to ⦋ l / k ⦌ B = Z$
27	26 5	suppss2	$⊢ φ \to (l \in A ⟼ ⦋ l / k ⦌ B) supp Z \subseteq W$
28	11 27	eqsstrid	$⊢ φ \to (k \in A ⟼ B) supp Z \subseteq W$

Metamath Proof Explorer

Theorem suppss2f

Proof