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	$$⊢\left(F:X⟶Y\wedge X\ne \varnothing \right)\to \left(F\ne \varnothing \wedge Y\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		f0dom0	$$⊢F:X⟶Y\to \left(X=\varnothing \leftrightarrow F=\varnothing \right)$$
2	1	necon3bid	$$⊢F:X⟶Y\to \left(X\ne \varnothing \leftrightarrow F\ne \varnothing \right)$$
3	2	biimpa	$$⊢\left(F:X⟶Y\wedge X\ne \varnothing \right)\to F\ne \varnothing$$
4		feq3	$$⊢Y=\varnothing \to \left(F:X⟶Y\leftrightarrow F:X⟶\varnothing \right)$$
5		f00	$$⊢F:X⟶\varnothing \leftrightarrow \left(F=\varnothing \wedge X=\varnothing \right)$$
6	5	simprbi	$$⊢F:X⟶\varnothing \to X=\varnothing$$
7	4 6	biimtrdi	$$⊢Y=\varnothing \to \left(F:X⟶Y\to X=\varnothing \right)$$
8		nne	$$⊢\neg X\ne \varnothing \leftrightarrow X=\varnothing$$
9	7 8	imbitrrdi	$$⊢Y=\varnothing \to \left(F:X⟶Y\to \neg X\ne \varnothing \right)$$
10		imnan	$$⊢\left(F:X⟶Y\to \neg X\ne \varnothing \right)\leftrightarrow \neg \left(F:X⟶Y\wedge X\ne \varnothing \right)$$
11	9 10	sylib	$$⊢Y=\varnothing \to \neg \left(F:X⟶Y\wedge X\ne \varnothing \right)$$
12	11	necon2ai	$$⊢\left(F:X⟶Y\wedge X\ne \varnothing \right)\to Y\ne \varnothing$$
13	3 12	jca	$$⊢\left(F:X⟶Y\wedge X\ne \varnothing \right)\to \left(F\ne \varnothing \wedge Y\ne \varnothing \right)$$