Metamath Proof Explorer


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 SV0SWordV

Proof

Step Hyp Ref Expression
1 0zd SV0
2 id SVSV
3 1 2 fsnd SV0S:0V
4 fzo01 0..^1=0
5 4 feq2i 0S:0..^1V0S:0V
6 3 5 sylibr SV0S:0..^1V
7 iswrdi 0S:0..^1V0SWordV
8 6 7 syl SV0SWordV