Metamath Proof Explorer

Theorem wrdlen1

Description: A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018) (Proof shortened by AV, 19-Oct-2018)

Ref Expression
Assertion wrdlen1 ⊢ W ∈ Word V ∧ W = 1 → ∃ v ∈ V W ⁡ 0 = v

Proof

Step Hyp Ref Expression
1 1le1 ⊢ 1 ≤ 1
2 breq2 ⊢ W = 1 → 1 ≤ W ↔ 1 ≤ 1
3 1 2 mpbiri ⊢ W = 1 → 1 ≤ W
4 wrdsymb1 ⊢ W ∈ Word V ∧ 1 ≤ W → W ⁡ 0 ∈ V
5 3 4 sylan2 ⊢ W ∈ Word V ∧ W = 1 → W ⁡ 0 ∈ V
6 clel5 ⊢ W ⁡ 0 ∈ V ↔ ∃ v ∈ V W ⁡ 0 = v
7 5 6 sylib ⊢ W ∈ Word V ∧ W = 1 → ∃ v ∈ V W ⁡ 0 = v