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

Metamath Proof Explorer

Theorem eliman0

Description: A nonempty function value is an element of the image of the function. (Contributed by Thierry Arnoux, 25-Jun-2019)

Ref Expression
Assertion eliman0 ( ( 𝐴 ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvbr0 ⊢ ( 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ∨ ( 𝐹 ‘ 𝐴 ) = ∅ )
2 orcom ⊢ ( ( 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ∨ ( 𝐹 ‘ 𝐴 ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝐴 ) = ∅ ∨ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
3 1 2 mpbi ⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ ∨ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) )
4 3 ori ⊢ ( ¬ ( 𝐹 ‘ 𝐴 ) = ∅ → 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) )
5 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) ↔ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) )
6 5 rspcev ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 𝐹 ( 𝐹 ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) )
7 4 6 sylan2 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) )
8 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
9 8 elima ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑥 𝐹 ( 𝐹 ‘ 𝐴 ) )
10 7 9 sylibr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ¬ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐹 “ 𝐵 ) )