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 ⊢ W ∈ Word V ∧ U ∈ X ∧ ∀ s ∈ V W ++ ⟨“ s ”⟩ ∈ X → S = s ∧ ∀ x ∈ X x ∈ Word V ∧ x = W + 1 → W = U prefix W → U = W ++ ⟨“ S ”⟩

Proof

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