Metamath Proof Explorer


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 syl5bb ( ( 𝑅𝑦 ) ∈ V → ( 𝑧 = ( 𝑅𝑦 ) ↔ 𝑦 ( 𝑥 ∈ V ↦ ( 𝑅𝑥 ) ) 𝑧 ) )
33 20 32 syl5bb ( ( 𝑅𝑦 ) ∈ 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 ↦ ( 𝑅𝑥 ) )