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 e. Word V /\ U e. X ) /\ A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = U -> ( x e. Word V <-> U e. Word V ) )
2 fveqeq2 
 |-  ( x = U -> ( ( # ` x ) = ( ( # ` W ) + 1 ) <-> ( # ` U ) = ( ( # ` W ) + 1 ) ) )
3 1 2 anbi12d 
 |-  ( x = U -> ( ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) <-> ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) )
4 3 rspcv 
 |-  ( U e. X -> ( A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) -> ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) )
5 4 adantl 
 |-  ( ( W e. Word V /\ U e. X ) -> ( A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) -> ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) )
6 simpl 
 |-  ( ( W e. Word V /\ U e. X ) -> W e. Word V )
7 6 adantr 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> W e. Word V )
8 simpl 
 |-  ( ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> U e. Word V )
9 8 adantl 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> U e. Word V )
10 simprr 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> ( # ` U ) = ( ( # ` W ) + 1 ) )
11 ccats1pfxeqrex 
 |-  ( ( W e. Word V /\ U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> E. u e. V U = ( W ++ <" u "> ) ) )
12 7 9 10 11 syl3anc 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> E. u e. 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 "> ) e. X <-> ( W ++ <" u "> ) e. X ) )
16 eqeq2 
 |-  ( s = u -> ( S = s <-> S = u ) )
17 15 16 imbi12d 
 |-  ( s = u -> ( ( ( W ++ <" s "> ) e. X -> S = s ) <-> ( ( W ++ <" u "> ) e. X -> S = u ) ) )
18 17 rspcv 
 |-  ( u e. V -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> ( ( W ++ <" u "> ) e. X -> S = u ) ) )
19 eleq1 
 |-  ( U = ( W ++ <" u "> ) -> ( U e. X <-> ( W ++ <" u "> ) e. X ) )
20 id 
 |-  ( ( ( W ++ <" u "> ) e. X -> S = u ) -> ( ( W ++ <" u "> ) e. X -> S = u ) )
21 20 imp 
 |-  ( ( ( ( W ++ <" u "> ) e. X -> S = u ) /\ ( W ++ <" u "> ) e. X ) -> S = u )
22 21 eqcomd 
 |-  ( ( ( ( W ++ <" u "> ) e. X -> S = u ) /\ ( W ++ <" u "> ) e. X ) -> u = S )
23 22 s1eqd 
 |-  ( ( ( ( W ++ <" u "> ) e. X -> S = u ) /\ ( W ++ <" u "> ) e. X ) -> <" u "> = <" S "> )
24 23 oveq2d 
 |-  ( ( ( ( W ++ <" u "> ) e. X -> S = u ) /\ ( W ++ <" u "> ) e. X ) -> ( W ++ <" u "> ) = ( W ++ <" S "> ) )
25 24 eqeq2d 
 |-  ( ( ( ( W ++ <" u "> ) e. X -> S = u ) /\ ( W ++ <" u "> ) e. X ) -> ( U = ( W ++ <" u "> ) <-> U = ( W ++ <" S "> ) ) )
26 25 biimpd 
 |-  ( ( ( ( W ++ <" u "> ) e. X -> S = u ) /\ ( W ++ <" u "> ) e. X ) -> ( U = ( W ++ <" u "> ) -> U = ( W ++ <" S "> ) ) )
27 26 ex 
 |-  ( ( ( W ++ <" u "> ) e. X -> S = u ) -> ( ( W ++ <" u "> ) e. X -> ( U = ( W ++ <" u "> ) -> U = ( W ++ <" S "> ) ) ) )
28 27 com13 
 |-  ( U = ( W ++ <" u "> ) -> ( ( W ++ <" u "> ) e. X -> ( ( ( W ++ <" u "> ) e. X -> S = u ) -> U = ( W ++ <" S "> ) ) ) )
29 19 28 sylbid 
 |-  ( U = ( W ++ <" u "> ) -> ( U e. X -> ( ( ( W ++ <" u "> ) e. X -> S = u ) -> U = ( W ++ <" S "> ) ) ) )
30 29 com3l 
 |-  ( U e. X -> ( ( ( W ++ <" u "> ) e. X -> S = u ) -> ( U = ( W ++ <" u "> ) -> U = ( W ++ <" S "> ) ) ) )
31 18 30 sylan9r 
 |-  ( ( U e. X /\ u e. V ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> ( U = ( W ++ <" u "> ) -> U = ( W ++ <" S "> ) ) ) )
32 31 com23 
 |-  ( ( U e. X /\ u e. V ) -> ( U = ( W ++ <" u "> ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> U = ( W ++ <" S "> ) ) ) )
33 32 rexlimdva 
 |-  ( U e. X -> ( E. u e. V U = ( W ++ <" u "> ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> U = ( W ++ <" S "> ) ) ) )
34 33 adantl 
 |-  ( ( W e. Word V /\ U e. X ) -> ( E. u e. V U = ( W ++ <" u "> ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> U = ( W ++ <" S "> ) ) ) )
35 34 adantr 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> ( E. u e. V U = ( W ++ <" u "> ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> U = ( W ++ <" S "> ) ) ) )
36 12 35 syld 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> U = ( W ++ <" S "> ) ) ) )
37 36 com23 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) ) )
38 37 ex 
 |-  ( ( W e. Word V /\ U e. X ) -> ( ( U e. Word V /\ ( # ` U ) = ( ( # ` W ) + 1 ) ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) ) ) )
39 5 38 syld 
 |-  ( ( W e. Word V /\ U e. X ) -> ( A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) ) ) )
40 39 com23 
 |-  ( ( W e. Word V /\ U e. X ) -> ( A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) -> ( A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) ) ) )
41 40 3imp 
 |-  ( ( ( W e. Word V /\ U e. X ) /\ A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( U prefix ( # ` W ) ) -> U = ( W ++ <" S "> ) ) )