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

Metamath Proof Explorer

Theorem feldmfvelcdm

Description: A class is an element of the domain iff it's function value is an element of the codomain of a function. (Contributed by AV, 22-Apr-2025)

Ref Expression
Assertion feldmfvelcdm ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝑋 ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 1 ffvelcdmda ⊢ ( ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 )
3 2 ex ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝑋 ∈ 𝐴 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )
4 df-nel ⊢ ( ∅ ∉ 𝐵 ↔ ¬ ∅ ∈ 𝐵 )
5 nelelne ⊢ ( ¬ ∅ ∈ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ∅ ) )
6 4 5 sylbi ⊢ ( ∅ ∉ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) ≠ ∅ ) )
7 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
8 fvfundmfvn0 ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) )
9 simprl ⊢ ( ( dom 𝐹 = 𝐴 ∧ ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) ) → 𝑋 ∈ dom 𝐹 )
10 simpl ⊢ ( ( dom 𝐹 = 𝐴 ∧ ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) ) → dom 𝐹 = 𝐴 )
11 9 10 eleqtrd ⊢ ( ( dom 𝐹 = 𝐴 ∧ ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) ) → 𝑋 ∈ 𝐴 )
12 11 ex ⊢ ( dom 𝐹 = 𝐴 → ( ( 𝑋 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝑋 } ) ) → 𝑋 ∈ 𝐴 ) )
13 7 8 12 syl2im ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ 𝐴 ) )
14 6 13 sylan9r ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 → 𝑋 ∈ 𝐴 ) )
15 3 14 impbid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∅ ∉ 𝐵 ) → ( 𝑋 ∈ 𝐴 ↔ ( 𝐹 ‘ 𝑋 ) ∈ 𝐵 ) )