cnvimadfsn

Description: The support of functions "defined" by inverse images expressed by binary relations. (Contributed by AV, 7-Apr-2019)

		Ref	Expression
	Assertion	cnvimadfsn	$⊢ R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (x R y \land y \neq Z)\}$

Step	Hyp	Ref	Expression
1		dfima3	$⊢ R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (y \in (V ∖ \{Z\}) \land ⟨y, x⟩ \in R^{-1})\}$
2		eldifvsn	$⊢ y \in V \to (y \in (V ∖ \{Z\}) \leftrightarrow y \neq Z)$
3	2	elv	$⊢ y \in (V ∖ \{Z\}) \leftrightarrow y \neq Z$
4		vex	$⊢ y \in V$
5		vex	$⊢ x \in V$
6	4 5	opelcnv	$⊢ ⟨y, x⟩ \in R^{-1} \leftrightarrow ⟨x, y⟩ \in R$
7		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
8	6 7	bitr4i	$⊢ ⟨y, x⟩ \in R^{-1} \leftrightarrow x R y$
9	3 8	anbi12ci	$⊢ (y \in (V ∖ \{Z\}) \land ⟨y, x⟩ \in R^{-1}) \leftrightarrow (x R y \land y \neq Z)$
10	9	exbii	$⊢ \exists y (y \in (V ∖ \{Z\}) \land ⟨y, x⟩ \in R^{-1}) \leftrightarrow \exists y (x R y \land y \neq Z)$
11	10	abbii	$⊢ \{x \| \exists y (y \in (V ∖ \{Z\}) \land ⟨y, x⟩ \in R^{-1})\} = \{x \| \exists y (x R y \land y \neq Z)\}$
12	1 11	eqtri	$⊢ R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (x R y \land y \neq Z)\}$

Metamath Proof Explorer