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

Metamath Proof Explorer

Theorem fdomne0

Description: A function with non-empty domain is non-empty and has non-empty codomain. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Assertion fdomne0 ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) → ( 𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 f0dom0 ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 = ∅ ↔ 𝐹 = ∅ ) )
2 1 necon3bid ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( 𝑋 ≠ ∅ ↔ 𝐹 ≠ ∅ ) )
3 2 biimpa ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) → 𝐹 ≠ ∅ )
4 feq3 ⊢ ( 𝑌 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 ↔ 𝐹 : 𝑋 ⟶ ∅ ) )
5 f00 ⊢ ( 𝐹 : 𝑋 ⟶ ∅ ↔ ( 𝐹 = ∅ ∧ 𝑋 = ∅ ) )
6 5 simprbi ⊢ ( 𝐹 : 𝑋 ⟶ ∅ → 𝑋 = ∅ )
7 4 6 biimtrdi ⊢ ( 𝑌 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 → 𝑋 = ∅ ) )
8 nne ⊢ ( ¬ 𝑋 ≠ ∅ ↔ 𝑋 = ∅ )
9 7 8 imbitrrdi ⊢ ( 𝑌 = ∅ → ( 𝐹 : 𝑋 ⟶ 𝑌 → ¬ 𝑋 ≠ ∅ ) )
10 imnan ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 → ¬ 𝑋 ≠ ∅ ) ↔ ¬ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) )
11 9 10 sylib ⊢ ( 𝑌 = ∅ → ¬ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) )
12 11 necon2ai ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) → 𝑌 ≠ ∅ )
13 3 12 jca ⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) → ( 𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅ ) )