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 𝐹 𝑥 = ( 𝐹 ‘ 𝑌 ) ) )