Metamath Proof Explorer

Theorem fvelimad

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

Ref Expression
Hypotheses fvelimad.x 
|- F/_ x F
fvelimad.f 
|- ( ph -> F Fn A )
fvelimad.c 
|- ( ph -> C e. ( F " B ) )
Assertion fvelimad 
|- ( ph -> E. x e. ( A i^i B ) ( F ` x ) = C )

Proof

Step Hyp Ref Expression
1 fvelimad.x 
 |-  F/_ x F
2 fvelimad.f 
 |-  ( ph -> F Fn A )
3 fvelimad.c 
 |-  ( ph -> C e. ( F " B ) )
4 elimag 
 |-  ( C e. ( F " B ) -> ( C e. ( F " B ) <-> E. y e. B y F C ) )
5 4 ibi 
 |-  ( C e. ( F " B ) -> E. y e. B y F C )
6 3 5 syl 
 |-  ( ph -> E. y e. B y F C )
7 nfv 
 |-  F/ y ph
8 nfre1 
 |-  F/ y E. y e. ( A i^i B ) ( F ` y ) = C
9 vex 
 |-  y e. _V
10 9 a1i 
 |-  ( ( ph /\ y F C ) -> y e. _V )
11 3 adantr 
 |-  ( ( ph /\ y F C ) -> C e. ( F " B ) )
12 simpr 
 |-  ( ( ph /\ y F C ) -> y F C )
13 10 11 12 breldmd 
 |-  ( ( ph /\ y F C ) -> y e. dom F )
14 2 fndmd 
 |-  ( ph -> dom F = A )
15 14 adantr 
 |-  ( ( ph /\ y F C ) -> dom F = A )
16 13 15 eleqtrd 
 |-  ( ( ph /\ y F C ) -> y e. A )
17 16 3adant2 
 |-  ( ( ph /\ y e. B /\ y F C ) -> y e. A )
18 simp2 
 |-  ( ( ph /\ y e. B /\ y F C ) -> y e. B )
19 17 18 elind 
 |-  ( ( ph /\ y e. B /\ y F C ) -> y e. ( A i^i B ) )
20 fnfun 
 |-  ( F Fn A -> Fun F )
21 2 20 syl 
 |-  ( ph -> Fun F )
22 21 3ad2ant1 
 |-  ( ( ph /\ y e. B /\ y F C ) -> Fun F )
23 simp3 
 |-  ( ( ph /\ y e. B /\ y F C ) -> y F C )
24 funbrfv 
 |-  ( Fun F -> ( y F C -> ( F ` y ) = C ) )
25 22 23 24 sylc 
 |-  ( ( ph /\ y e. B /\ y F C ) -> ( F ` y ) = C )
26 rspe 
 |-  ( ( y e. ( A i^i B ) /\ ( F ` y ) = C ) -> E. y e. ( A i^i B ) ( F ` y ) = C )
27 19 25 26 syl2anc 
 |-  ( ( ph /\ y e. B /\ y F C ) -> E. y e. ( A i^i B ) ( F ` y ) = C )
28 27 3exp 
 |-  ( ph -> ( y e. B -> ( y F C -> E. y e. ( A i^i B ) ( F ` y ) = C ) ) )
29 7 8 28 rexlimd 
 |-  ( ph -> ( E. y e. B y F C -> E. y e. ( A i^i B ) ( F ` y ) = C ) )
30 6 29 mpd 
 |-  ( ph -> E. y e. ( A i^i B ) ( F ` y ) = C )
31 nfv 
 |-  F/ y ( F ` x ) = C
32 nfcv 
 |-  F/_ x y
33 1 32 nffv 
 |-  F/_ x ( F ` y )
34 33 nfeq1 
 |-  F/ x ( F ` y ) = C
35 fveqeq2 
 |-  ( x = y -> ( ( F ` x ) = C <-> ( F ` y ) = C ) )
36 31 34 35 cbvrexw 
 |-  ( E. x e. ( A i^i B ) ( F ` x ) = C <-> E. y e. ( A i^i B ) ( F ` y ) = C )
37 30 36 sylibr 
 |-  ( ph -> E. x e. ( A i^i B ) ( F ` x ) = C )