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 ( ♯ ‘ 𝑊 ) ) → 𝑈 = ( 𝑊 ++ ⟨“ 𝑆 ”⟩ ) ) )