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	⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 0 , 𝑆 ⟩ } ∈ Word 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		0zd	⊢ ( 𝑆 ∈ 𝑉 → 0 ∈ ℤ )
2		id	⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ 𝑉 )
3	1 2	fsnd	⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 0 , 𝑆 ⟩ } : { 0 } ⟶ 𝑉 )
4		fzo01	⊢ ( 0 ..^ 1 ) = { 0 }
5	4	feq2i	⊢ ( { ⟨ 0 , 𝑆 ⟩ } : ( 0 ..^ 1 ) ⟶ 𝑉 ↔ { ⟨ 0 , 𝑆 ⟩ } : { 0 } ⟶ 𝑉 )
6	3 5	sylibr	⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 0 , 𝑆 ⟩ } : ( 0 ..^ 1 ) ⟶ 𝑉 )
7		iswrdi	⊢ ( { ⟨ 0 , 𝑆 ⟩ } : ( 0 ..^ 1 ) ⟶ 𝑉 → { ⟨ 0 , 𝑆 ⟩ } ∈ Word 𝑉 )
8	6 7	syl	⊢ ( 𝑆 ∈ 𝑉 → { ⟨ 0 , 𝑆 ⟩ } ∈ Word 𝑉 )