Theorem 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	⊢ Image 𝑅 Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }

Proof

Step	Hyp	Ref	Expression
1		funimage	⊢ Fun Image 𝑅
2		vex	⊢ 𝑦 ∈ V
3		vex	⊢ 𝑥 ∈ V
4	2 3	brimage	⊢ ( 𝑦 Image 𝑅 𝑥 ↔ 𝑥 = ( 𝑅 “ 𝑦 ) )
5		eqvisset	⊢ ( 𝑥 = ( 𝑅 “ 𝑦 ) → ( 𝑅 “ 𝑦 ) ∈ V )
6	4 5	sylbi	⊢ ( 𝑦 Image 𝑅 𝑥 → ( 𝑅 “ 𝑦 ) ∈ V )
7	6	exlimiv	⊢ ( ∃ 𝑥 𝑦 Image 𝑅 𝑥 → ( 𝑅 “ 𝑦 ) ∈ V )
8		eqid	⊢ ( 𝑅 “ 𝑦 ) = ( 𝑅 “ 𝑦 )
9		brimageg	⊢ ( ( 𝑦 ∈ V ∧ ( 𝑅 “ 𝑦 ) ∈ V ) → ( 𝑦 Image 𝑅 ( 𝑅 “ 𝑦 ) ↔ ( 𝑅 “ 𝑦 ) = ( 𝑅 “ 𝑦 ) ) )
10	2 9	mpan	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( 𝑦 Image 𝑅 ( 𝑅 “ 𝑦 ) ↔ ( 𝑅 “ 𝑦 ) = ( 𝑅 “ 𝑦 ) ) )
11	8 10	mpbiri	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → 𝑦 Image 𝑅 ( 𝑅 “ 𝑦 ) )
12		breq2	⊢ ( 𝑥 = ( 𝑅 “ 𝑦 ) → ( 𝑦 Image 𝑅 𝑥 ↔ 𝑦 Image 𝑅 ( 𝑅 “ 𝑦 ) ) )
13	12	spcegv	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( 𝑦 Image 𝑅 ( 𝑅 “ 𝑦 ) → ∃ 𝑥 𝑦 Image 𝑅 𝑥 ) )
14	11 13	mpd	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ∃ 𝑥 𝑦 Image 𝑅 𝑥 )
15	7 14	impbii	⊢ ( ∃ 𝑥 𝑦 Image 𝑅 𝑥 ↔ ( 𝑅 “ 𝑦 ) ∈ V )
16	2	eldm	⊢ ( 𝑦 ∈ dom Image 𝑅 ↔ ∃ 𝑥 𝑦 Image 𝑅 𝑥 )
17		imaeq2	⊢ ( 𝑥 = 𝑦 → ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝑦 ) )
18	17	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 “ 𝑥 ) ∈ V ↔ ( 𝑅 “ 𝑦 ) ∈ V ) )
19	2 18	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ↔ ( 𝑅 “ 𝑦 ) ∈ V )
20	15 16 19	3bitr4i	⊢ ( 𝑦 ∈ dom Image 𝑅 ↔ 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } )
21	20	eqriv	⊢ dom Image 𝑅 = { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }
22		df-fn	⊢ ( Image 𝑅 Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ↔ ( Fun Image 𝑅 ∧ dom Image 𝑅 = { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ) )
23	1 21 22	mpbir2an	⊢ Image 𝑅 Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }