Metamath Proof Explorer

Theorem fvelimad

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

Ref Expression
Hypotheses fvelimad.x ⊢ Ⅎ _ x F
fvelimad.f ⊢ φ → F Fn A
fvelimad.c ⊢ φ → C ∈ F B
Assertion fvelimad ⊢ φ → ∃ x ∈ A ∩ B F ⁡ x = C

Proof

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