Theorem snopiswrd

Description: A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018) (Proof shortened by AV, 18-Apr-2021)

	Ref	Expression
Assertion	snopiswrd	$$⊢S\in V\to \left\{⟨0,S⟩\right\}\in \mathrm{Word}V$$

Proof

Step	Hyp	Ref	Expression
1		0zd	$$⊢S\in V\to 0\in \mathbb{Z}$$
2		id	$$⊢S\in V\to S\in V$$
3	1 2	fsnd	$$⊢S\in V\to \left\{⟨0,S⟩\right\}:\left\{0\right\}⟶V$$
4		fzo01	$$⊢\left(0..^1\right)=\left\{0\right\}$$
5	4	feq2i	$$⊢\left\{⟨0,S⟩\right\}:\left(0..^1\right)⟶V\leftrightarrow \left\{⟨0,S⟩\right\}:\left\{0\right\}⟶V$$
6	3 5	sylibr	$$⊢S\in V\to \left\{⟨0,S⟩\right\}:\left(0..^1\right)⟶V$$
7		iswrdi	$$⊢\left\{⟨0,S⟩\right\}:\left(0..^1\right)⟶V\to \left\{⟨0,S⟩\right\}\in \mathrm{Word}V$$
8	6 7	syl	$$⊢S\in V\to \left\{⟨0,S⟩\right\}\in \mathrm{Word}V$$