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 ⊢ 𝖨𝗆𝖺𝗀𝖾 R = x ∈ V ⟼ R x

Proof

Step Hyp Ref Expression
1 funimage ⊢ Fun ⁡ 𝖨𝗆𝖺𝗀𝖾 R
2 funrel ⊢ Fun ⁡ 𝖨𝗆𝖺𝗀𝖾 R → Rel ⁡ 𝖨𝗆𝖺𝗀𝖾 R
3 1 2 ax-mp ⊢ Rel ⁡ 𝖨𝗆𝖺𝗀𝖾 R
4 mptrel ⊢ Rel ⁡ x ∈ V ⟼ R x
5 vex ⊢ y ∈ V
6 vex ⊢ z ∈ V
7 5 6 breldm ⊢ y 𝖨𝗆𝖺𝗀𝖾 R z → y ∈ dom ⁡ 𝖨𝗆𝖺𝗀𝖾 R
8 fnimage ⊢ 𝖨𝗆𝖺𝗀𝖾 R Fn x | R x ∈ V
9 8 fndmi ⊢ dom ⁡ 𝖨𝗆𝖺𝗀𝖾 R = x | R x ∈ V
10 7 9 eleqtrdi ⊢ y 𝖨𝗆𝖺𝗀𝖾 R z → y ∈ x | R x ∈ V
11 5 6 breldm ⊢ y x ∈ V ⟼ R x z → y ∈ dom ⁡ x ∈ V ⟼ R x
12 eqid ⊢ x ∈ V ⟼ R x = x ∈ V ⟼ R x
13 12 dmmpt ⊢ dom ⁡ x ∈ V ⟼ R x = x ∈ V | R x ∈ V
14 rabab ⊢ x ∈ V | R x ∈ V = x | R x ∈ V
15 13 14 eqtri ⊢ dom ⁡ x ∈ V ⟼ R x = x | R x ∈ V
16 11 15 eleqtrdi ⊢ y x ∈ V ⟼ R x z → y ∈ x | R x ∈ V
17 imaeq2 ⊢ x = y → R x = R y
18 17 eleq1d ⊢ x = y → R x ∈ V ↔ R y ∈ V
19 5 18 elab ⊢ y ∈ x | R x ∈ V ↔ R y ∈ V
20 5 6 brimage ⊢ y 𝖨𝗆𝖺𝗀𝖾 R z ↔ z = R y
21 eqcom ⊢ z = R y ↔ R y = z
22 17 12 fvmptg ⊢ y ∈ V ∧ R y ∈ V → x ∈ V ⟼ R x ⁡ y = R y
23 5 22 mpan ⊢ R y ∈ V → x ∈ V ⟼ R x ⁡ y = R y
24 23 eqeq1d ⊢ R y ∈ V → x ∈ V ⟼ R x ⁡ y = z ↔ R y = z
25 funmpt ⊢ Fun ⁡ x ∈ V ⟼ R x
26 df-fn ⊢ x ∈ V ⟼ R x Fn x | R x ∈ V ↔ Fun ⁡ x ∈ V ⟼ R x ∧ dom ⁡ x ∈ V ⟼ R x = x | R x ∈ V
27 25 15 26 mpbir2an ⊢ x ∈ V ⟼ R x Fn x | R x ∈ V
28 19 biimpri ⊢ R y ∈ V → y ∈ x | R x ∈ V
29 fnbrfvb ⊢ x ∈ V ⟼ R x Fn x | R x ∈ V ∧ y ∈ x | R x ∈ V → x ∈ V ⟼ R x ⁡ y = z ↔ y x ∈ V ⟼ R x z
30 27 28 29 sylancr ⊢ R y ∈ V → x ∈ V ⟼ R x ⁡ y = z ↔ y x ∈ V ⟼ R x z
31 24 30 bitr3d ⊢ R y ∈ V → R y = z ↔ y x ∈ V ⟼ R x z
32 21 31 bitrid ⊢ R y ∈ V → z = R y ↔ y x ∈ V ⟼ R x z
33 20 32 bitrid ⊢ R y ∈ V → y 𝖨𝗆𝖺𝗀𝖾 R z ↔ y x ∈ V ⟼ R x z
34 19 33 sylbi ⊢ y ∈ x | R x ∈ V → y 𝖨𝗆𝖺𝗀𝖾 R z ↔ y x ∈ V ⟼ R x z
35 10 16 34 pm5.21nii ⊢ y 𝖨𝗆𝖺𝗀𝖾 R z ↔ y x ∈ V ⟼ R x z
36 3 4 35 eqbrriv ⊢ 𝖨𝗆𝖺𝗀𝖾 R = x ∈ V ⟼ R x