suppimacnvss

Description: The support of functions "defined" by inverse images is a subset of the support defined by df-supp . (Contributed by AV, 7-Apr-2019)

		Ref	Expression
	Assertion	suppimacnvss	$⊢ (R \in V \land Z \in W) \to R^{-1} [V ∖ \{Z\}] \subseteq R supp Z$

Step	Hyp	Ref	Expression
1		exsimpl	$⊢ \exists y (x R y \land y \neq Z) \to \exists y x R y$
2		pm5.1	$⊢ (x R y \land y \neq Z) \to (x R y \leftrightarrow y \neq Z)$
3	2	eximi	$⊢ \exists y (x R y \land y \neq Z) \to \exists y (x R y \leftrightarrow y \neq Z)$
4	1 3	jca	$⊢ \exists y (x R y \land y \neq Z) \to (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))$
5	4	a1i	$⊢ (R \in V \land Z \in W) \to (\exists y (x R y \land y \neq Z) \to (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z)))$
6	5	ss2abdv	$⊢ (R \in V \land Z \in W) \to \{x \| \exists y (x R y \land y \neq Z)\} \subseteq \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$
7		cnvimadfsn	$⊢ R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (x R y \land y \neq Z)\}$
8	7	a1i	$⊢ (R \in V \land Z \in W) \to R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (x R y \land y \neq Z)\}$
9		suppvalbr	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \| (\exists y x R y \land \exists y (x R y \leftrightarrow y \neq Z))\}$
10	6 8 9	3sstr4d	$⊢ (R \in V \land Z \in W) \to R^{-1} [V ∖ \{Z\}] \subseteq R supp Z$

Metamath Proof Explorer