Metamath Proof Explorer

Theorem ccats1alpha

Description: A concatenation of a word with a singleton word is a word over an alphabet S iff the symbols of both words belong to the alphabet S . (Contributed by AV, 27-Mar-2022)

Ref Expression
Assertion ccats1alpha ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐴 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 wrdv ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐴 ∈ Word V )
2 s1cli ⊢ ⟨“ 𝑋 ”⟩ ∈ Word V
3 2 a1i ⊢ ( 𝑋 ∈ 𝑈 → ⟨“ 𝑋 ”⟩ ∈ Word V )
4 ccatalpha ⊢ ( ( 𝐴 ∈ Word V ∧ ⟨“ 𝑋 ”⟩ ∈ Word V ) → ( ( 𝐴 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ) )
5 1 3 4 syl2an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐴 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ) )
6 simpr ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) → ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 )
7 s1len ⊢ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1
8 wrdl1exs1 ⊢ ( ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ∧ ( ♯ ‘ ⟨“ 𝑋 ”⟩ ) = 1 ) → ∃ 𝑤 ∈ 𝑆 ⟨“ 𝑋 ”⟩ = ⟨“ 𝑤 ”⟩ )
9 6 7 8 sylancl ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) → ∃ 𝑤 ∈ 𝑆 ⟨“ 𝑋 ”⟩ = ⟨“ 𝑤 ”⟩ )
10 elex ⊢ ( 𝑋 ∈ 𝑈 → 𝑋 ∈ V )
11 10 adantr ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) → 𝑋 ∈ V )
12 elex ⊢ ( 𝑤 ∈ 𝑆 → 𝑤 ∈ V )
13 s111 ⊢ ( ( 𝑋 ∈ V ∧ 𝑤 ∈ V ) → ( ⟨“ 𝑋 ”⟩ = ⟨“ 𝑤 ”⟩ ↔ 𝑋 = 𝑤 ) )
14 11 12 13 syl2an ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ∧ 𝑤 ∈ 𝑆 ) → ( ⟨“ 𝑋 ”⟩ = ⟨“ 𝑤 ”⟩ ↔ 𝑋 = 𝑤 ) )
15 simpr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ 𝑆 )
16 eleq1 ⊢ ( 𝑋 = 𝑤 → ( 𝑋 ∈ 𝑆 ↔ 𝑤 ∈ 𝑆 ) )
17 15 16 syl5ibrcom ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑋 = 𝑤 → 𝑋 ∈ 𝑆 ) )
18 14 17 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ∧ 𝑤 ∈ 𝑆 ) → ( ⟨“ 𝑋 ”⟩ = ⟨“ 𝑤 ”⟩ → 𝑋 ∈ 𝑆 ) )
19 18 rexlimdva ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) → ( ∃ 𝑤 ∈ 𝑆 ⟨“ 𝑋 ”⟩ = ⟨“ 𝑤 ”⟩ → 𝑋 ∈ 𝑆 ) )
20 9 19 mpd ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) → 𝑋 ∈ 𝑆 )
21 20 ex ⊢ ( 𝑋 ∈ 𝑈 → ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 → 𝑋 ∈ 𝑆 ) )
22 s1cl ⊢ ( 𝑋 ∈ 𝑆 → ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 )
23 21 22 impbid1 ⊢ ( 𝑋 ∈ 𝑈 → ( ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ↔ 𝑋 ∈ 𝑆 ) )
24 23 anbi2d ⊢ ( 𝑋 ∈ 𝑈 → ( ( 𝐴 ∈ Word 𝑆 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆 ) ) )
25 24 adantl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐴 ∈ Word 𝑆 ∧ ⟨“ 𝑋 ”⟩ ∈ Word 𝑆 ) ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆 ) ) )
26 5 25 bitrd ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑈 ) → ( ( 𝐴 ++ ⟨“ 𝑋 ”⟩ ) ∈ Word 𝑆 ↔ ( 𝐴 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆 ) ) )