0wrd0

Description: The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018)

		Ref	Expression
	Assertion	0wrd0	$⊢ W \in Word \emptyset \leftrightarrow W = \emptyset$

Step	Hyp	Ref	Expression
1		wrdf	$⊢ W \in Word \emptyset \to W : (0 ..^\|W\|) ⟶ \emptyset$
2		f00	$⊢ W : (0 ..^\|W\|) ⟶ \emptyset \leftrightarrow (W = \emptyset \land (0 ..^\|W\|) = \emptyset)$
3	2	simplbi	$⊢ W : (0 ..^\|W\|) ⟶ \emptyset \to W = \emptyset$
4	1 3	syl	$⊢ W \in Word \emptyset \to W = \emptyset$
5		wrd0	$⊢ \emptyset \in Word \emptyset$
6		eleq1	$⊢ W = \emptyset \to (W \in Word \emptyset \leftrightarrow \emptyset \in Word \emptyset)$
7	5 6	mpbiri	$⊢ W = \emptyset \to W \in Word \emptyset$
8	4 7	impbii	$⊢ W \in Word \emptyset \leftrightarrow W = \emptyset$

Metamath Proof Explorer