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

Metamath Proof Explorer

Theorem fvelimab

Description: Function value in an image. (Contributed by NM, 20-Jan-2007) (Proof shortened by Andrew Salmon, 22-Oct-2011) (Revised by David Abernethy, 17-Dec-2011)

Ref Expression
Assertion fvelimab ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) → 𝐶 ∈ V )
2 1 anim2i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝐶 ∈ ( 𝐹 “ 𝐵 ) ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝐶 ∈ V ) )
3 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
4 eleq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∈ V ↔ 𝐶 ∈ V ) )
5 3 4 mpbii ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝐶 → 𝐶 ∈ V )
6 5 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 → 𝐶 ∈ V )
7 6 anim2i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) → ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝐶 ∈ V ) )
8 eleq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ 𝐶 ∈ ( 𝐹 “ 𝐵 ) ) )
9 eqeq2 ⊢ ( 𝑦 = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )
10 9 rexbidv ⊢ ( 𝑦 = 𝐶 → ( ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )
11 8 10 bibi12d ⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) )
12 11 imbi2d ⊢ ( 𝑦 = 𝐶 → ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) ) )
13 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
14 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
15 14 sseq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ⊆ dom 𝐹 ↔ 𝐵 ⊆ 𝐴 ) )
16 15 biimpar ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ dom 𝐹 )
17 dfimafn ⊢ ( ( Fun 𝐹 ∧ 𝐵 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
18 13 16 17 syl2an2r ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐹 “ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 } )
19 18 eqabrd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
20 12 19 vtoclg ⊢ ( 𝐶 ∈ V → ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) )
21 20 impcom ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝐶 ∈ V ) → ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )
22 2 7 21 pm5.21nd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = 𝐶 ) )