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 syl6bi ( 𝑋 = ∅ → ( 𝐹 : 𝑋𝑌𝐹 = ∅ ) )
5 4 com12 ( 𝐹 : 𝑋𝑌 → ( 𝑋 = ∅ → 𝐹 = ∅ ) )
6 feq1 ( 𝐹 = ∅ → ( 𝐹 : 𝑋𝑌 ↔ ∅ : 𝑋𝑌 ) )
7 fdm ( ∅ : 𝑋𝑌 → dom ∅ = 𝑋 )
8 dm0 dom ∅ = ∅
9 7 8 eqtr3di ( ∅ : 𝑋𝑌𝑋 = ∅ )
10 6 9 syl6bi ( 𝐹 = ∅ → ( 𝐹 : 𝑋𝑌𝑋 = ∅ ) )
11 10 com12 ( 𝐹 : 𝑋𝑌 → ( 𝐹 = ∅ → 𝑋 = ∅ ) )
12 5 11 impbid ( 𝐹 : 𝑋𝑌 → ( 𝑋 = ∅ ↔ 𝐹 = ∅ ) )