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	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ( 𝐹 ‘ 𝑥 ) = 𝐶 )