Metamath Proof Explorer

Theorem eqs1

Description: A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion eqs1 ⊢W∈WordA∧W=1→W=⟨“W⁡0”⟩

Proof

Step Hyp Ref Expression
1 id ⊢W=1→W=1
2 s1len ⊢⟨“W⁡0”⟩=1
3 1 2 eqtr4di ⊢W=1→W=⟨“W⁡0”⟩
4 fvex ⊢W⁡0∈V
5 s1fv ⊢W⁡0∈V→⟨“W⁡0”⟩⁡0=W⁡0
6 4 5 ax-mp ⊢⟨“W⁡0”⟩⁡0=W⁡0
7 6 eqcomi ⊢W⁡0=⟨“W⁡0”⟩⁡0
8 c0ex ⊢0∈V
9 fveq2 ⊢x=0→W⁡x=W⁡0
10 fveq2 ⊢x=0→⟨“W⁡0”⟩⁡x=⟨“W⁡0”⟩⁡0
11 9 10 eqeq12d ⊢x=0→W⁡x=⟨“W⁡0”⟩⁡x↔W⁡0=⟨“W⁡0”⟩⁡0
12 8 11 ralsn ⊢∀x∈0W⁡x=⟨“W⁡0”⟩⁡x↔W⁡0=⟨“W⁡0”⟩⁡0
13 7 12 mpbir ⊢∀x∈0W⁡x=⟨“W⁡0”⟩⁡x
14 oveq2 ⊢W=1→0..^W=0..^1
15 fzo01 ⊢0..^1=0
16 14 15 eqtrdi ⊢W=1→0..^W=0
17 16 raleqdv ⊢W=1→∀x∈0..^WW⁡x=⟨“W⁡0”⟩⁡x↔∀x∈0W⁡x=⟨“W⁡0”⟩⁡x
18 13 17 mpbiri ⊢W=1→∀x∈0..^WW⁡x=⟨“W⁡0”⟩⁡x
19 3 18 jca ⊢W=1→W=⟨“W⁡0”⟩∧∀x∈0..^WW⁡x=⟨“W⁡0”⟩⁡x
20 s1cli ⊢⟨“W⁡0”⟩∈WordV
21 eqwrd ⊢W∈WordA∧⟨“W⁡0”⟩∈WordV→W=⟨“W⁡0”⟩↔W=⟨“W⁡0”⟩∧∀x∈0..^WW⁡x=⟨“W⁡0”⟩⁡x
22 20 21 mpan2 ⊢W∈WordA→W=⟨“W⁡0”⟩↔W=⟨“W⁡0”⟩∧∀x∈0..^WW⁡x=⟨“W⁡0”⟩⁡x
23 19 22 imbitrrid ⊢W∈WordA→W=1→W=⟨“W⁡0”⟩
24 23 imp ⊢W∈WordA∧W=1→W=⟨“W⁡0”⟩