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

Metamath Proof Explorer

Theorem f0dom0

Description: A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019)

Ref Expression
Assertion f0dom0 ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ ↔ 𝐹 = ∅ ) )

Proof

Step Hyp Ref Expression
1 feq2 ⊢ ( 𝑋 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 ↔ 𝐹 : ∅ ⟶ 𝑌 ) )
2 f0bi ⊢ ( 𝐹 : ∅ ⟶ 𝑌 ↔ 𝐹 = ∅ )
3 2 biimpi ⊢ ( 𝐹 : ∅ ⟶ 𝑌 → 𝐹 = ∅ )
4 1 3 biimtrdi ⊢ ( 𝑋 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝐹 = ∅ ) )
5 4 com12 ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ → 𝐹 = ∅ ) )
6 feq1 ⊢ ( 𝐹 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 ↔ ∅ : 𝑋 ⟶ 𝑌 ) )
7 fdm ⊢ ( ∅ : 𝑋 ⟶ 𝑌 → dom ∅ = 𝑋 )
8 dm0 ⊢ dom ∅ = ∅
9 7 8 eqtr3di ⊢ ( ∅ : 𝑋 ⟶ 𝑌 → 𝑋 = ∅ )
10 6 9 biimtrdi ⊢ ( 𝐹 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝑋 = ∅ ) )
11 10 com12 ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝐹 = ∅ → 𝑋 = ∅ ) )
12 5 11 impbid ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ ↔ 𝐹 = ∅ ) )