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

Metamath Proof Explorer

Theorem fvelima2

Description: Function value in an image. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion fvelima2 ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ ( 𝐹 “ 𝐶 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 elimag ⊢ ( 𝐵 ∈ ( 𝐹 “ 𝐶 ) → ( 𝐵 ∈ ( 𝐹 “ 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐶 𝑥 𝐹 𝐵 ) )
2 1 ibi ⊢ ( 𝐵 ∈ ( 𝐹 “ 𝐶 ) → ∃ 𝑥 ∈ 𝐶 𝑥 𝐹 𝐵 )
3 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐶 𝑥 𝐹 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) )
4 2 3 sylib ⊢ ( 𝐵 ∈ ( 𝐹 “ 𝐶 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) )
5 fnbr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 𝐹 𝐵 ) → 𝑥 ∈ 𝐴 )
6 5 adantrl ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → 𝑥 ∈ 𝐴 )
7 simprl ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → 𝑥 ∈ 𝐶 )
8 6 7 elind ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) )
9 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
10 funbrfv ⊢ ( Fun 𝐹 → ( 𝑥 𝐹 𝐵 → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
11 10 imp ⊢ ( ( Fun 𝐹 ∧ 𝑥 𝐹 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
12 9 11 sylan ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 𝐹 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
13 12 adantrl ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
14 8 13 jca ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
15 14 ex ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) → ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) ) )
16 15 eximdv ⊢ ( 𝐹 Fn 𝐴 → ( ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) ) )
17 16 imp ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
18 df-rex ⊢ ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐵 ) )
19 17 18 sylibr ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∃ 𝑥 ( 𝑥 ∈ 𝐶 ∧ 𝑥 𝐹 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = 𝐵 )
20 4 19 sylan2 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ ( 𝐹 “ 𝐶 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐶 ) ( 𝐹 ‘ 𝑥 ) = 𝐵 )