Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 funimage ⊢ Fun ⁡ 𝖨𝗆𝖺𝗀𝖾 R
2 vex ⊢ y ∈ V
3 vex ⊢ x ∈ V
4 2 3 brimage ⊢ y 𝖨𝗆𝖺𝗀𝖾 R x ↔ x = R y
5 eqvisset ⊢ x = R y → R y ∈ V
6 4 5 sylbi ⊢ y 𝖨𝗆𝖺𝗀𝖾 R x → R y ∈ V
7 6 exlimiv ⊢ ∃ x y 𝖨𝗆𝖺𝗀𝖾 R x → R y ∈ V
8 eqid ⊢ R y = R y
9 brimageg ⊢ y ∈ V ∧ R y ∈ V → y 𝖨𝗆𝖺𝗀𝖾 R R y ↔ R y = R y
10 2 9 mpan ⊢ R y ∈ V → y 𝖨𝗆𝖺𝗀𝖾 R R y ↔ R y = R y
11 8 10 mpbiri ⊢ R y ∈ V → y 𝖨𝗆𝖺𝗀𝖾 R R y
12 breq2 ⊢ x = R y → y 𝖨𝗆𝖺𝗀𝖾 R x ↔ y 𝖨𝗆𝖺𝗀𝖾 R R y
13 12 spcegv ⊢ R y ∈ V → y 𝖨𝗆𝖺𝗀𝖾 R R y → ∃ x y 𝖨𝗆𝖺𝗀𝖾 R x
14 11 13 mpd ⊢ R y ∈ V → ∃ x y 𝖨𝗆𝖺𝗀𝖾 R x
15 7 14 impbii ⊢ ∃ x y 𝖨𝗆𝖺𝗀𝖾 R x ↔ R y ∈ V
16 2 eldm ⊢ y ∈ dom ⁡ 𝖨𝗆𝖺𝗀𝖾 R ↔ ∃ x y 𝖨𝗆𝖺𝗀𝖾 R x
17 imaeq2 ⊢ x = y → R x = R y
18 17 eleq1d ⊢ x = y → R x ∈ V ↔ R y ∈ V
19 2 18 elab ⊢ y ∈ x | R x ∈ V ↔ R y ∈ V
20 15 16 19 3bitr4i ⊢ y ∈ dom ⁡ 𝖨𝗆𝖺𝗀𝖾 R ↔ y ∈ x | R x ∈ V
21 20 eqriv ⊢ dom ⁡ 𝖨𝗆𝖺𝗀𝖾 R = x | R x ∈ V
22 df-fn ⊢ 𝖨𝗆𝖺𝗀𝖾 R Fn x | R x ∈ V ↔ Fun ⁡ 𝖨𝗆𝖺𝗀𝖾 R ∧ dom ⁡ 𝖨𝗆𝖺𝗀𝖾 R = x | R x ∈ V
23 1 21 22 mpbir2an ⊢ 𝖨𝗆𝖺𝗀𝖾 R Fn x | R x ∈ V