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

Metamath Proof Explorer

Theorem fvelimad

Description: Function value in an image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses fvelimad.x ⊢ Ⅎ 𝑥 𝐹
fvelimad.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
fvelimad.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 “ 𝐵 ) )
Assertion fvelimad ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 fvelimad.x ⊢ Ⅎ 𝑥 𝐹
2 fvelimad.f ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3 fvelimad.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 “ 𝐵 ) )
4 elimag ⊢ ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) → ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑦 𝐹 𝐶 ) )
5 4 ibi ⊢ ( 𝐶 ∈ ( 𝐹 “ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 𝑦 𝐹 𝐶 )
6 3 5 syl ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝑦 𝐹 𝐶 )
7 nfv ⊢ Ⅎ 𝑦 𝜑
8 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶
9 vex ⊢ 𝑦 ∈ V
10 9 a1i ⊢ ( ( 𝜑 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 ∈ V )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 𝐹 𝐶 ) → 𝐶 ∈ ( 𝐹 “ 𝐵 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 𝐹 𝐶 )
13 10 11 12 breldmd ⊢ ( ( 𝜑 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 ∈ dom 𝐹 )
14 2 fndmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑦 𝐹 𝐶 ) → dom 𝐹 = 𝐴 )
16 13 15 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 ∈ 𝐴 )
17 16 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 ∈ 𝐴 )
18 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 ∈ 𝐵 )
19 17 18 elind ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) )
20 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
21 2 20 syl ⊢ ( 𝜑 → Fun 𝐹 )
22 21 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → Fun 𝐹 )
23 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → 𝑦 𝐹 𝐶 )
24 funbrfv ⊢ ( Fun 𝐹 → ( 𝑦 𝐹 𝐶 → ( 𝐹 ‘ 𝑦 ) = 𝐶 ) )
25 22 23 24 sylc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → ( 𝐹 ‘ 𝑦 ) = 𝐶 )
26 rspe ⊢ ( ( 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) = 𝐶 ) → ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶 )
27 19 25 26 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦 𝐹 𝐶 ) → ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶 )
28 27 3exp ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → ( 𝑦 𝐹 𝐶 → ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶 ) ) )
29 7 8 28 rexlimd ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐵 𝑦 𝐹 𝐶 → ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶 ) )
30 6 29 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶 )
31 nfv ⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) = 𝐶
32 nfcv ⊢ Ⅎ 𝑥 𝑦
33 1 32 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 )
34 33 nfeq1 ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) = 𝐶
35 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( 𝐹 ‘ 𝑦 ) = 𝐶 ) )
36 31 34 35 cbvrexw ⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ∃ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑦 ) = 𝐶 )
37 30 36 sylibr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝐶 )