Metamath Proof Explorer

Theorem suppiniseg

Description: Relation between the support ( F supp Z ) and the initial segment (`' F " { Z } ) ` . (Contributed by Thierry Arnoux, 25-Jun-2024)

		Ref	Expression
	Assertion	suppiniseg	$⊢ (Fun F \land F \in V \land Z \in W) \to dom F ∖ {supp}_{Z} (F) = F^{-1} [\{Z\}]$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ x \in (dom F ∖ {supp}_{Z} (F)) \leftrightarrow (x \in dom F \land \neg x \in {supp}_{Z} (F))$
2		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
3	2	biimpi	$⊢ Fun F \to F Fn dom F$
4		elsuppfng	$⊢ (F Fn dom F \land F \in V \land Z \in W) \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in dom F \land F (x) \neq Z))$
5	3 4	syl3an1	$⊢ (Fun F \land F \in V \land Z \in W) \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in dom F \land F (x) \neq Z))$
6	5	baibd	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (x \in {supp}_{Z} (F) \leftrightarrow F (x) \neq Z)$
7	6	notbid	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (\neg x \in {supp}_{Z} (F) \leftrightarrow \neg F (x) \neq Z)$
8		nne	$⊢ \neg F (x) \neq Z \leftrightarrow F (x) = Z$
9	7 8	bitrdi	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (\neg x \in {supp}_{Z} (F) \leftrightarrow F (x) = Z)$
10		fvex	$⊢ F (x) \in V$
11	10	elsn	$⊢ F (x) \in \{Z\} \leftrightarrow F (x) = Z$
12	9 11	bitr4di	$⊢ ((Fun F \land F \in V \land Z \in W) \land x \in dom F) \to (\neg x \in {supp}_{Z} (F) \leftrightarrow F (x) \in \{Z\})$
13	12	pm5.32da	$⊢ (Fun F \land F \in V \land Z \in W) \to ((x \in dom F \land \neg x \in {supp}_{Z} (F)) \leftrightarrow (x \in dom F \land F (x) \in \{Z\}))$
14	1 13	bitrid	$⊢ (Fun F \land F \in V \land Z \in W) \to (x \in (dom F ∖ {supp}_{Z} (F)) \leftrightarrow (x \in dom F \land F (x) \in \{Z\}))$
15	3	3ad2ant1	$⊢ (Fun F \land F \in V \land Z \in W) \to F Fn dom F$
16		elpreima	$⊢ F Fn dom F \to (x \in F^{-1} [\{Z\}] \leftrightarrow (x \in dom F \land F (x) \in \{Z\}))$
17	15 16	syl	$⊢ (Fun F \land F \in V \land Z \in W) \to (x \in F^{-1} [\{Z\}] \leftrightarrow (x \in dom F \land F (x) \in \{Z\}))$
18	14 17	bitr4d	$⊢ (Fun F \land F \in V \land Z \in W) \to (x \in (dom F ∖ {supp}_{Z} (F)) \leftrightarrow x \in F^{-1} [\{Z\}])$
19	18	eqrdv	$⊢ (Fun F \land F \in V \land Z \in W) \to dom F ∖ {supp}_{Z} (F) = F^{-1} [\{Z\}]$