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	⊢ ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ 𝑋 ≠ ∅ ) → ( 𝐹 ≠ ∅ ∧ 𝑌 ≠ ∅ ) )