fnimage

Description: Image R is a function over the set-like portion of R . (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	fnimage	$⊢ 𝖨𝗆𝖺𝗀𝖾 R Fn \{x \| R [x] \in V\}$

Proof

Step	Hyp	Ref	Expression
1		funimage	$⊢ Fun 𝖨𝗆𝖺𝗀𝖾 R$
2		vex	$⊢ y \in V$
3		vex	$⊢ x \in V$
4	2 3	brimage	$⊢ y 𝖨𝗆𝖺𝗀𝖾 R x \leftrightarrow x = R [y]$
5		eqvisset	$⊢ x = R [y] \to R [y] \in V$
6	4 5	sylbi	$⊢ y 𝖨𝗆𝖺𝗀𝖾 R x \to R [y] \in V$
7	6	exlimiv	$⊢ \exists x y 𝖨𝗆𝖺𝗀𝖾 R x \to R [y] \in V$
8		eqid	$⊢ R [y] = R [y]$
9		brimageg	$⊢ (y \in V \land R [y] \in V) \to (y 𝖨𝗆𝖺𝗀𝖾 R R [y] \leftrightarrow R [y] = R [y])$
10	2 9	mpan	$⊢ R [y] \in V \to (y 𝖨𝗆𝖺𝗀𝖾 R R [y] \leftrightarrow R [y] = R [y])$
11	8 10	mpbiri	$⊢ R [y] \in V \to y 𝖨𝗆𝖺𝗀𝖾 R R [y]$
12		breq2	$⊢ x = R [y] \to (y 𝖨𝗆𝖺𝗀𝖾 R x \leftrightarrow y 𝖨𝗆𝖺𝗀𝖾 R R [y])$
13	12	spcegv	$⊢ R [y] \in V \to (y 𝖨𝗆𝖺𝗀𝖾 R R [y] \to \exists x y 𝖨𝗆𝖺𝗀𝖾 R x)$
14	11 13	mpd	$⊢ R [y] \in V \to \exists x y 𝖨𝗆𝖺𝗀𝖾 R x$
15	7 14	impbii	$⊢ \exists x y 𝖨𝗆𝖺𝗀𝖾 R x \leftrightarrow R [y] \in V$
16	2	eldm	$⊢ y \in dom 𝖨𝗆𝖺𝗀𝖾 R \leftrightarrow \exists x y 𝖨𝗆𝖺𝗀𝖾 R x$
17		imaeq2	$⊢ x = y \to R [x] = R [y]$
18	17	eleq1d	$⊢ x = y \to (R [x] \in V \leftrightarrow R [y] \in V)$
19	2 18	elab	$⊢ y \in \{x \| R [x] \in V\} \leftrightarrow R [y] \in V$
20	15 16 19	3bitr4i	$⊢ y \in dom 𝖨𝗆𝖺𝗀𝖾 R \leftrightarrow y \in \{x \| R [x] \in V\}$
21	20	eqriv	$⊢ dom 𝖨𝗆𝖺𝗀𝖾 R = \{x \| R [x] \in V\}$
22		df-fn	$⊢ 𝖨𝗆𝖺𝗀𝖾 R Fn \{x \| R [x] \in V\} \leftrightarrow (Fun 𝖨𝗆𝖺𝗀𝖾 R \land dom 𝖨𝗆𝖺𝗀𝖾 R = \{x \| R [x] \in V\})$
23	1 21 22	mpbir2an	$⊢ 𝖨𝗆𝖺𝗀𝖾 R Fn \{x \| R [x] \in V\}$

Metamath Proof Explorer

Theorem fnimage

Proof