Theorem funeldmb

Description: If (/) is not part of the range of a function F , then A is in the domain of F iff ( FA ) =/= (/) . (Contributed by Scott Fenton, 7-Dec-2021)

	Ref	Expression
Assertion	funeldmb	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹 ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ‘ 𝐴 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fvelrn	⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 )
2	1	ex	⊢ ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) )
3	2	adantr	⊢ ( ( Fun 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ) )
4		eleq1	⊢ ( ( 𝐹 ‘ 𝐴 ) = ∅ → ( ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ↔ ∅ ∈ ran 𝐹 ) )
5	4	adantl	⊢ ( ( Fun 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ran 𝐹 ↔ ∅ ∈ ran 𝐹 ) )
6	3 5	sylibd	⊢ ( ( Fun 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( 𝐴 ∈ dom 𝐹 → ∅ ∈ ran 𝐹 ) )
7	6	con3d	⊢ ( ( Fun 𝐹 ∧ ( 𝐹 ‘ 𝐴 ) = ∅ ) → ( ¬ ∅ ∈ ran 𝐹 → ¬ 𝐴 ∈ dom 𝐹 ) )
8	7	impancom	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = ∅ → ¬ 𝐴 ∈ dom 𝐹 ) )
9		ndmfv	⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ )
10	8 9	impbid1	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) = ∅ ↔ ¬ 𝐴 ∈ dom 𝐹 ) )
11	10	necon2abid	⊢ ( ( Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹 ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ‘ 𝐴 ) ≠ ∅ ) )