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 ∈ Word A ∧ 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 ∈ 0 W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x ↔ W ⁡ 0 = ⟨“ W ⁡ 0 ”⟩ ⁡ 0
13 7 12 mpbir ⊢ ∀ x ∈ 0 W ⁡ 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 ..^ W W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x ↔ ∀ x ∈ 0 W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x
18 13 17 mpbiri ⊢ W = 1 → ∀ x ∈ 0 ..^ W W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x
19 3 18 jca ⊢ W = 1 → W = ⟨“ W ⁡ 0 ”⟩ ∧ ∀ x ∈ 0 ..^ W W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x
20 s1cli ⊢ ⟨“ W ⁡ 0 ”⟩ ∈ Word V
21 eqwrd ⊢ W ∈ Word A ∧ ⟨“ W ⁡ 0 ”⟩ ∈ Word V → W = ⟨“ W ⁡ 0 ”⟩ ↔ W = ⟨“ W ⁡ 0 ”⟩ ∧ ∀ x ∈ 0 ..^ W W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x
22 20 21 mpan2 ⊢ W ∈ Word A → W = ⟨“ W ⁡ 0 ”⟩ ↔ W = ⟨“ W ⁡ 0 ”⟩ ∧ ∀ x ∈ 0 ..^ W W ⁡ x = ⟨“ W ⁡ 0 ”⟩ ⁡ x
23 19 22 imbitrrid ⊢ W ∈ Word A → W = 1 → W = ⟨“ W ⁡ 0 ”⟩
24 23 imp ⊢ W ∈ Word A ∧ W = 1 → W = ⟨“ W ⁡ 0 ”⟩