Metamath Proof Explorer


Theorem reuccatpfxs1lem

Description: Lemma for reuccatpfxs1 . (Contributed by Alexander van der Vekens, 5-Oct-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion reuccatpfxs1lem ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) ∧ ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ( 𝑥 = 𝑈 → ( 𝑥 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ) )
2 fveqeq2 ( 𝑥 = 𝑈 → ( ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ↔ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) )
3 1 2 anbi12d ( 𝑥 = 𝑈 → ( ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ↔ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) )
4 3 rspcv ( 𝑈𝑋 → ( ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) )
5 4 adantl ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) → ( ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) )
6 simpl ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) → 𝑊 ∈ Word 𝑉 )
7 6 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → 𝑊 ∈ Word 𝑉 )
8 simpl ( ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → 𝑈 ∈ Word 𝑉 )
9 8 adantl ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → 𝑈 ∈ Word 𝑉 )
10 simprr ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) )
11 ccats1pfxeqrex ( ( 𝑊 ∈ Word 𝑉𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ∃ 𝑢𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ) )
12 7 9 10 11 syl3anc ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ∃ 𝑢𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ) )
13 s1eq ( 𝑠 = 𝑢 → ⟨“ 𝑠 ”⟩ = ⟨“ 𝑢 ”⟩ )
14 13 oveq2d ( 𝑠 = 𝑢 → ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) )
15 14 eleq1d ( 𝑠 = 𝑢 → ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋 ↔ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) )
16 eqeq2 ( 𝑠 = 𝑢 → ( 𝑆 = 𝑠𝑆 = 𝑢 ) )
17 15 16 imbi12d ( 𝑠 = 𝑢 → ( ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) ↔ ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ) )
18 17 rspcv ( 𝑢𝑉 → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ) )
19 eleq1 ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( 𝑈𝑋 ↔ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) )
20 id ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) → ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) )
21 20 imp ( ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ∧ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) → 𝑆 = 𝑢 )
22 21 eqcomd ( ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ∧ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) → 𝑢 = 𝑆 )
23 22 s1eqd ( ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ∧ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) → ⟨“ 𝑢 ”⟩ = ⟨“ 𝑆 ”⟩ )
24 23 oveq2d ( ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ∧ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) → ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) )
25 24 eqeq2d ( ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ∧ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) → ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ↔ 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) )
26 25 biimpd ( ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) ∧ ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 ) → ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) )
27 26 ex ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) → ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
28 27 com13 ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋 → ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
29 19 28 sylbid ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( 𝑈𝑋 → ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
30 29 com3l ( 𝑈𝑋 → ( ( ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) ∈ 𝑋𝑆 = 𝑢 ) → ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
31 18 30 sylan9r ( ( 𝑈𝑋𝑢𝑉 ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
32 31 com23 ( ( 𝑈𝑋𝑢𝑉 ) → ( 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
33 32 rexlimdva ( 𝑈𝑋 → ( ∃ 𝑢𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
34 33 adantl ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) → ( ∃ 𝑢𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
35 34 adantr ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∃ 𝑢𝑉 𝑈 = ( 𝑊 ++ ⟨“ 𝑢 ”⟩ ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
36 12 35 syld ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
37 36 com23 ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) )
38 37 ex ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) → ( ( 𝑈 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑈 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) ) )
39 5 38 syld ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) → ( ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) ) )
40 39 com23 ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) → ( ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) → ( ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) ) ) )
41 40 3imp ( ( ( 𝑊 ∈ Word 𝑉𝑈𝑋 ) ∧ ∀ 𝑠𝑉 ( ( 𝑊 ++ ⟨“ 𝑠 ”⟩ ) ∈ 𝑋𝑆 = 𝑠 ) ∧ ∀ 𝑥𝑋 ( 𝑥 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑥 ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) ) → ( 𝑊 = ( 𝑈 prefix ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) )