Theorem imageval

Description: The image functor in maps-to notation. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	imageval	⊢ Image 𝑅 = ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		funimage	⊢ Fun Image 𝑅
2		funrel	⊢ ( Fun Image 𝑅 → Rel Image 𝑅 )
3	1 2	ax-mp	⊢ Rel Image 𝑅
4		mptrel	⊢ Rel ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) )
5		vex	⊢ 𝑦 ∈ V
6		vex	⊢ 𝑧 ∈ V
7	5 6	breldm	⊢ ( 𝑦 Image 𝑅 𝑧 → 𝑦 ∈ dom Image 𝑅 )
8		fnimage	⊢ Image 𝑅 Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }
9	8	fndmi	⊢ dom Image 𝑅 = { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }
10	7 9	eleqtrdi	⊢ ( 𝑦 Image 𝑅 𝑧 → 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } )
11	5 6	breldm	⊢ ( 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 → 𝑦 ∈ dom ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) )
12		eqid	⊢ ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) = ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) )
13	12	dmmpt	⊢ dom ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) = { 𝑥 ∈ V ∣ ( 𝑅 “ 𝑥 ) ∈ V }
14		rabab	⊢ { 𝑥 ∈ V ∣ ( 𝑅 “ 𝑥 ) ∈ V } = { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }
15	13 14	eqtri	⊢ dom ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) = { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }
16	11 15	eleqtrdi	⊢ ( 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 → 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } )
17		imaeq2	⊢ ( 𝑥 = 𝑦 → ( 𝑅 “ 𝑥 ) = ( 𝑅 “ 𝑦 ) )
18	17	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑅 “ 𝑥 ) ∈ V ↔ ( 𝑅 “ 𝑦 ) ∈ V ) )
19	5 18	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ↔ ( 𝑅 “ 𝑦 ) ∈ V )
20	5 6	brimage	⊢ ( 𝑦 Image 𝑅 𝑧 ↔ 𝑧 = ( 𝑅 “ 𝑦 ) )
21		eqcom	⊢ ( 𝑧 = ( 𝑅 “ 𝑦 ) ↔ ( 𝑅 “ 𝑦 ) = 𝑧 )
22	17 12	fvmptg	⊢ ( ( 𝑦 ∈ V ∧ ( 𝑅 “ 𝑦 ) ∈ V ) → ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑅 “ 𝑦 ) )
23	5 22	mpan	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) ‘ 𝑦 ) = ( 𝑅 “ 𝑦 ) )
24	23	eqeq1d	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) ‘ 𝑦 ) = 𝑧 ↔ ( 𝑅 “ 𝑦 ) = 𝑧 ) )
25		funmpt	⊢ Fun ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) )
26		df-fn	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ↔ ( Fun ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) ∧ dom ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) = { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ) )
27	25 15 26	mpbir2an	⊢ ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V }
28	19	biimpri	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } )
29		fnbrfvb	⊢ ( ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) Fn { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ∧ 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } ) → ( ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) ‘ 𝑦 ) = 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 ) )
30	27 28 29	sylancr	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( ( ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) ‘ 𝑦 ) = 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 ) )
31	24 30	bitr3d	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( ( 𝑅 “ 𝑦 ) = 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 ) )
32	21 31	bitrid	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( 𝑧 = ( 𝑅 “ 𝑦 ) ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 ) )
33	20 32	bitrid	⊢ ( ( 𝑅 “ 𝑦 ) ∈ V → ( 𝑦 Image 𝑅 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 ) )
34	19 33	sylbi	⊢ ( 𝑦 ∈ { 𝑥 ∣ ( 𝑅 “ 𝑥 ) ∈ V } → ( 𝑦 Image 𝑅 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 ) )
35	10 16 34	pm5.21nii	⊢ ( 𝑦 Image 𝑅 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) ) 𝑧 )
36	3 4 35	eqbrriv	⊢ Image 𝑅 = ( 𝑥 ∈ V ↦ ( 𝑅 “ 𝑥 ) )