Description: A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | s2cld.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) | |
| s2cld.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 ) | ||
| s3cld.3 | ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 ) | ||
| s4cld.4 | ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 ) | ||
| s5cld.5 | ⊢ ( 𝜑 → 𝐸 ∈ 𝑋 ) | ||
| s6cld.6 | ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 ) | ||
| s7cld.7 | ⊢ ( 𝜑 → 𝐺 ∈ 𝑋 ) | ||
| s8cld.8 | ⊢ ( 𝜑 → 𝐻 ∈ 𝑋 ) | ||
| Assertion | s8cld | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ ∈ Word 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | s2cld.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) | |
| 2 | s2cld.2 | ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 ) | |
| 3 | s3cld.3 | ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 ) | |
| 4 | s4cld.4 | ⊢ ( 𝜑 → 𝐷 ∈ 𝑋 ) | |
| 5 | s5cld.5 | ⊢ ( 𝜑 → 𝐸 ∈ 𝑋 ) | |
| 6 | s6cld.6 | ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 ) | |
| 7 | s7cld.7 | ⊢ ( 𝜑 → 𝐺 ∈ 𝑋 ) | |
| 8 | s8cld.8 | ⊢ ( 𝜑 → 𝐻 ∈ 𝑋 ) | |
| 9 | df-s8 | ⊢ ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ = ( ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ++ ⟨“ 𝐻 ”⟩ ) | |
| 10 | 1 2 3 4 5 6 7 | s7cld | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 ”⟩ ∈ Word 𝑋 ) |
| 11 | 9 10 8 | cats1cld | ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 𝐷 𝐸 𝐹 𝐺 𝐻 ”⟩ ∈ Word 𝑋 ) |