Metamath Proof Explorer


Theorem eldmrexrnb

Description: For any element in the domain of a function, there is an element in the range of the function which is the value of the function at that element. Because of the definition df-fv of the value of a function, the theorem is only valid in general if the empty set is not contained in the range of the function (the implication "to the right" is always valid). Indeed, with the definition df-fv of the value of a function, ( FY ) = (/) may mean that the value of F at Y is the empty set or that F is not defined at Y . (Contributed by Alexander van der Vekens, 17-Dec-2017)

Ref Expression
Assertion eldmrexrnb ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( 𝑌 ∈ dom 𝐹 ↔ ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 eldmrexrn ( Fun 𝐹 → ( 𝑌 ∈ dom 𝐹 → ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹𝑌 ) ) )
2 1 adantr ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( 𝑌 ∈ dom 𝐹 → ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹𝑌 ) ) )
3 eleq1 ( 𝑥 = ( 𝐹𝑌 ) → ( 𝑥 ∈ ran 𝐹 ↔ ( 𝐹𝑌 ) ∈ ran 𝐹 ) )
4 elnelne2 ( ( ( 𝐹𝑌 ) ∈ ran 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( 𝐹𝑌 ) ≠ ∅ )
5 n0 ( ( 𝐹𝑌 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝐹𝑌 ) )
6 elfvdm ( 𝑦 ∈ ( 𝐹𝑌 ) → 𝑌 ∈ dom 𝐹 )
7 6 exlimiv ( ∃ 𝑦 𝑦 ∈ ( 𝐹𝑌 ) → 𝑌 ∈ dom 𝐹 )
8 5 7 sylbi ( ( 𝐹𝑌 ) ≠ ∅ → 𝑌 ∈ dom 𝐹 )
9 4 8 syl ( ( ( 𝐹𝑌 ) ∈ ran 𝐹 ∧ ∅ ∉ ran 𝐹 ) → 𝑌 ∈ dom 𝐹 )
10 9 expcom ( ∅ ∉ ran 𝐹 → ( ( 𝐹𝑌 ) ∈ ran 𝐹𝑌 ∈ dom 𝐹 ) )
11 10 adantl ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( ( 𝐹𝑌 ) ∈ ran 𝐹𝑌 ∈ dom 𝐹 ) )
12 11 com12 ( ( 𝐹𝑌 ) ∈ ran 𝐹 → ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → 𝑌 ∈ dom 𝐹 ) )
13 3 12 syl6bi ( 𝑥 = ( 𝐹𝑌 ) → ( 𝑥 ∈ ran 𝐹 → ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → 𝑌 ∈ dom 𝐹 ) ) )
14 13 com13 ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( 𝑥 ∈ ran 𝐹 → ( 𝑥 = ( 𝐹𝑌 ) → 𝑌 ∈ dom 𝐹 ) ) )
15 14 rexlimdv ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹𝑌 ) → 𝑌 ∈ dom 𝐹 ) )
16 2 15 impbid ( ( Fun 𝐹 ∧ ∅ ∉ ran 𝐹 ) → ( 𝑌 ∈ dom 𝐹 ↔ ∃ 𝑥 ∈ ran 𝐹 𝑥 = ( 𝐹𝑌 ) ) )