Theorem iswrddm0

Description: A function with empty domain is a word. (Contributed by AV, 13-Oct-2018)

	Ref	Expression
Assertion	iswrddm0	$$⊢W:\varnothing ⟶S\to W\in \mathrm{Word}S$$

Proof

Step	Hyp	Ref	Expression
1		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
2	1	feq2i	$$⊢W:\left(0..^0\right)⟶S\leftrightarrow W:\varnothing ⟶S$$
3		iswrdi	$$⊢W:\left(0..^0\right)⟶S\to W\in \mathrm{Word}S$$
4	2 3	sylbir	$$⊢W:\varnothing ⟶S\to W\in \mathrm{Word}S$$