This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 ↦ ( 𝑅 “ 𝑥 ) )