Theorem eldmrexrnb 7037

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 6497 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 6497 of the value of a function, (𝐹‘𝑌) = ∅ may mean that the value of 𝐹 at 𝑌 is the empty set or that 𝐹 is not defined at 𝑌. (Contributed by Alexander van der Vekens, 17-Dec-2017.)

Assertion

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

Distinct variable groups:   𝑥,𝐹   𝑥,𝑌

Proof of Theorem eldmrexrnb

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldmrexrn 7036	. . 3 ⊢ (Fun 𝐹 → (𝑌 ∈ dom 𝐹 → ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌)))
2	1	adantr 482	. 2 ⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → (𝑌 ∈ dom 𝐹 → ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌)))
3		eleq1 2829	. . . . 5 ⊢ (𝑥 = (𝐹‘𝑌) → (𝑥 ∈ ran 𝐹 ↔ (𝐹‘𝑌) ∈ ran 𝐹))
4		elnelne2 3052	. . . . . . . . 9 ⊢ (((𝐹‘𝑌) ∈ ran 𝐹 ∧ ∅ ∉ ran 𝐹) → (𝐹‘𝑌) ≠ ∅)
5		n0 4284	. . . . . . . . . 10 ⊢ ((𝐹‘𝑌) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑌))
6		elfvdm 6865	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝐹‘𝑌) → 𝑌 ∈ dom 𝐹)
7	6	exlimiv 1938	. . . . . . . . . 10 ⊢ (∃𝑦 𝑦 ∈ (𝐹‘𝑌) → 𝑌 ∈ dom 𝐹)
8	5, 7	sylbi 219	. . . . . . . . 9 ⊢ ((𝐹‘𝑌) ≠ ∅ → 𝑌 ∈ dom 𝐹)
9	4, 8	syl 17	. . . . . . . 8 ⊢ (((𝐹‘𝑌) ∈ ran 𝐹 ∧ ∅ ∉ ran 𝐹) → 𝑌 ∈ dom 𝐹)
10	9	expcom 415	. . . . . . 7 ⊢ (∅ ∉ ran 𝐹 → ((𝐹‘𝑌) ∈ ran 𝐹 → 𝑌 ∈ dom 𝐹))
11	10	adantl 483	. . . . . 6 ⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → ((𝐹‘𝑌) ∈ ran 𝐹 → 𝑌 ∈ dom 𝐹))
12	11	com12 32	. . . . 5 ⊢ ((𝐹‘𝑌) ∈ ran 𝐹 → ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → 𝑌 ∈ dom 𝐹))
13	3, 12	biimtrdi 255	. . . 4 ⊢ (𝑥 = (𝐹‘𝑌) → (𝑥 ∈ ran 𝐹 → ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → 𝑌 ∈ dom 𝐹)))
14	13	com13 88	. . 3 ⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → (𝑥 ∈ ran 𝐹 → (𝑥 = (𝐹‘𝑌) → 𝑌 ∈ dom 𝐹)))
15	14	rexlimdv 3140	. 2 ⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → (∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌) → 𝑌 ∈ dom 𝐹))
16	2, 15	impbid 214	1 ⊢ ((Fun 𝐹 ∧ ∅ ∉ ran 𝐹) → (𝑌 ∈ dom 𝐹 ↔ ∃𝑥 ∈ ran 𝐹 𝑥 = (𝐹‘𝑌)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ∃wex 1787   ∈ wcel 2121   ≠ wne 2936   ∉ wnel 3040  ∃wrex 3065  ∅c0 4264  dom cdm 5621  ran crn 5622  Fun wfun 6483  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by: (None)