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

Metamath Proof Explorer

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 𝐹 ↔ ( 𝐹 ‘ 𝐴 ) ≠ ∅ ) )