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

Metamath Proof Explorer

Theorem iswrddm0

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

		Ref	Expression
	Assertion	iswrddm0	$⊢ W : \emptyset ⟶ S \to W \in Word S$

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