ressupprn

Description: The range of a function restricted to its support. (Contributed by Thierry Arnoux, 25-Jun-2024)

		Ref	Expression
	Assertion	ressupprn	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = ran F ∖ \{\underset{˙}{0}\}$

Proof

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2	1	biimpi	$⊢ Fun F \to F Fn dom F$
3	2	3ad2ant1	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to F Fn dom F$
4		dmexg	$⊢ F \in V \to dom F \in V$
5	4	3ad2ant2	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to dom F \in V$
6		simp3	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to \underset{˙}{0} \in W$
7		elsuppfn	$⊢ (F Fn dom F \land dom F \in V \land \underset{˙}{0} \in W) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in dom F \land F (x) \neq \underset{˙}{0}))$
8	3 5 6 7	syl3anc	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to (x \in {supp}_{\underset{˙}{0}} (F) \leftrightarrow (x \in dom F \land F (x) \neq \underset{˙}{0}))$
9	8	anbi1d	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ((x \in {supp}_{\underset{˙}{0}} (F) \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y) \leftrightarrow ((x \in dom F \land F (x) \neq \underset{˙}{0}) \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y))$
10		anass	$⊢ ((x \in dom F \land F (x) \neq \underset{˙}{0}) \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y) \leftrightarrow (x \in dom F \land (F (x) \neq \underset{˙}{0} \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y))$
11	10	a1i	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to (((x \in dom F \land F (x) \neq \underset{˙}{0}) \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y) \leftrightarrow (x \in dom F \land (F (x) \neq \underset{˙}{0} \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y)))$
12	8	biimprd	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ((x \in dom F \land F (x) \neq \underset{˙}{0}) \to x \in {supp}_{\underset{˙}{0}} (F))$
13	12	impl	$⊢ (((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \land F (x) \neq \underset{˙}{0}) \to x \in {supp}_{\underset{˙}{0}} (F)$
14	13	fvresd	$⊢ (((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \land F (x) \neq \underset{˙}{0}) \to ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = F (x)$
15	14	eqeq1d	$⊢ (((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \land F (x) \neq \underset{˙}{0}) \to (({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y \leftrightarrow F (x) = y)$
16	15	pm5.32da	$⊢ ((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \to ((F (x) \neq \underset{˙}{0} \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y) \leftrightarrow (F (x) \neq \underset{˙}{0} \land F (x) = y))$
17		ancom	$⊢ (F (x) \neq \underset{˙}{0} \land F (x) = y) \leftrightarrow (F (x) = y \land F (x) \neq \underset{˙}{0})$
18		simpr	$⊢ (((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \land F (x) = y) \to F (x) = y$
19	18	neeq1d	$⊢ (((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \land F (x) = y) \to (F (x) \neq \underset{˙}{0} \leftrightarrow y \neq \underset{˙}{0})$
20	19	pm5.32da	$⊢ ((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \to ((F (x) = y \land F (x) \neq \underset{˙}{0}) \leftrightarrow (F (x) = y \land y \neq \underset{˙}{0}))$
21	17 20	syl5bb	$⊢ ((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \to ((F (x) \neq \underset{˙}{0} \land F (x) = y) \leftrightarrow (F (x) = y \land y \neq \underset{˙}{0}))$
22	16 21	bitrd	$⊢ ((Fun F \land F \in V \land \underset{˙}{0} \in W) \land x \in dom F) \to ((F (x) \neq \underset{˙}{0} \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y) \leftrightarrow (F (x) = y \land y \neq \underset{˙}{0}))$
23	22	pm5.32da	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ((x \in dom F \land (F (x) \neq \underset{˙}{0} \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y)) \leftrightarrow (x \in dom F \land (F (x) = y \land y \neq \underset{˙}{0})))$
24	9 11 23	3bitrd	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ((x \in {supp}_{\underset{˙}{0}} (F) \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y) \leftrightarrow (x \in dom F \land (F (x) = y \land y \neq \underset{˙}{0})))$
25	24	rexbidv2	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to (\exists x \in {supp}_{\underset{˙}{0}} (F) ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y \leftrightarrow \exists x \in dom F (F (x) = y \land y \neq \underset{˙}{0}))$
26		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
27		fnssres	$⊢ (F Fn dom F \land F supp \underset{˙}{0} \subseteq dom F) \to ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) Fn {supp}_{\underset{˙}{0}} (F)$
28	3 26 27	sylancl	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) Fn {supp}_{\underset{˙}{0}} (F)$
29		fvelrnb	$⊢ ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) Fn {supp}_{\underset{˙}{0}} (F) \to (y \in ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \leftrightarrow \exists x \in {supp}_{\underset{˙}{0}} (F) ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y)$
30	28 29	syl	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to (y \in ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \leftrightarrow \exists x \in {supp}_{\underset{˙}{0}} (F) ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) (x) = y)$
31		fvelrnb	$⊢ F Fn dom F \to (y \in ran F \leftrightarrow \exists x \in dom F F (x) = y)$
32	31	anbi1d	$⊢ F Fn dom F \to ((y \in ran F \land y \neq \underset{˙}{0}) \leftrightarrow (\exists x \in dom F F (x) = y \land y \neq \underset{˙}{0}))$
33		eldifsn	$⊢ y \in (ran F ∖ \{\underset{˙}{0}\}) \leftrightarrow (y \in ran F \land y \neq \underset{˙}{0})$
34		r19.41v	$⊢ \exists x \in dom F (F (x) = y \land y \neq \underset{˙}{0}) \leftrightarrow (\exists x \in dom F F (x) = y \land y \neq \underset{˙}{0})$
35	32 33 34	3bitr4g	$⊢ F Fn dom F \to (y \in (ran F ∖ \{\underset{˙}{0}\}) \leftrightarrow \exists x \in dom F (F (x) = y \land y \neq \underset{˙}{0}))$
36	3 35	syl	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to (y \in (ran F ∖ \{\underset{˙}{0}\}) \leftrightarrow \exists x \in dom F (F (x) = y \land y \neq \underset{˙}{0}))$
37	25 30 36	3bitr4d	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to (y \in ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \leftrightarrow y \in (ran F ∖ \{\underset{˙}{0}\}))$
38	37	eqrdv	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = ran F ∖ \{\underset{˙}{0}\}$

Metamath Proof Explorer

Theorem ressupprn

Proof