Metamath Proof Explorer

Theorem reuccatpfxs1

Description: There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Revised by AV, 13-Oct-2022)

Ref Expression
Hypothesis reuccatpfxs1.1 
|- F/_ v X
Assertion reuccatpfxs1 
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix ( # ` W ) ) ) )

Proof

Step Hyp Ref Expression
1 reuccatpfxs1.1 
 |-  F/_ v X
2 eleq1w 
 |-  ( x = y -> ( x e. Word V <-> y e. Word V ) )
3 fveqeq2 
 |-  ( x = y -> ( ( # ` x ) = ( ( # ` W ) + 1 ) <-> ( # ` y ) = ( ( # ` W ) + 1 ) ) )
4 2 3 anbi12d 
 |-  ( x = y -> ( ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) <-> ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) )
5 4 cbvralvw 
 |-  ( A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) <-> A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) )
6 1 nfel2 
 |-  F/ v ( W ++ <" u "> ) e. X
7 1 nfel2 
 |-  F/ v ( W ++ <" x "> ) e. X
8 s1eq 
 |-  ( v = x -> <" v "> = <" x "> )
9 8 oveq2d 
 |-  ( v = x -> ( W ++ <" v "> ) = ( W ++ <" x "> ) )
10 9 eleq1d 
 |-  ( v = x -> ( ( W ++ <" v "> ) e. X <-> ( W ++ <" x "> ) e. X ) )
11 s1eq 
 |-  ( x = u -> <" x "> = <" u "> )
12 11 oveq2d 
 |-  ( x = u -> ( W ++ <" x "> ) = ( W ++ <" u "> ) )
13 12 eleq1d 
 |-  ( x = u -> ( ( W ++ <" x "> ) e. X <-> ( W ++ <" u "> ) e. X ) )
14 6 7 10 13 reu8nf 
 |-  ( E! v e. V ( W ++ <" v "> ) e. X <-> E. v e. V ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) )
15 nfv 
 |-  F/ v W e. Word V
16 nfv 
 |-  F/ v ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) )
17 1 16 nfralw 
 |-  F/ v A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) )
18 15 17 nfan 
 |-  F/ v ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) )
19 nfv 
 |-  F/ v W = ( x prefix ( # ` W ) )
20 1 19 nfreuw 
 |-  F/ v E! x e. X W = ( x prefix ( # ` W ) )
21 simprl 
 |-  ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) -> ( W ++ <" v "> ) e. X )
22 simpl 
 |-  ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) -> W e. Word V )
23 22 ad2antrr 
 |-  ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) -> W e. Word V )
24 23 anim1i 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> ( W e. Word V /\ x e. X ) )
25 simplrr 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) )
26 simp-4r 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) )
27 reuccatpfxs1lem 
 |-  ( ( ( W e. Word V /\ x e. X ) /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) -> ( W = ( x prefix ( # ` W ) ) -> x = ( W ++ <" v "> ) ) )
28 24 25 26 27 syl3anc 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> ( W = ( x prefix ( # ` W ) ) -> x = ( W ++ <" v "> ) ) )
29 oveq1 
 |-  ( x = ( W ++ <" v "> ) -> ( x prefix ( # ` W ) ) = ( ( W ++ <" v "> ) prefix ( # ` W ) ) )
30 s1cl 
 |-  ( v e. V -> <" v "> e. Word V )
31 22 30 anim12i 
 |-  ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) -> ( W e. Word V /\ <" v "> e. Word V ) )
32 31 ad2antrr 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> ( W e. Word V /\ <" v "> e. Word V ) )
33 pfxccat1 
 |-  ( ( W e. Word V /\ <" v "> e. Word V ) -> ( ( W ++ <" v "> ) prefix ( # ` W ) ) = W )
34 32 33 syl 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> ( ( W ++ <" v "> ) prefix ( # ` W ) ) = W )
35 29 34 sylan9eqr 
 |-  ( ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) /\ x = ( W ++ <" v "> ) ) -> ( x prefix ( # ` W ) ) = W )
36 35 eqcomd 
 |-  ( ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) /\ x = ( W ++ <" v "> ) ) -> W = ( x prefix ( # ` W ) ) )
37 36 ex 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> ( x = ( W ++ <" v "> ) -> W = ( x prefix ( # ` W ) ) ) )
38 28 37 impbid 
 |-  ( ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) /\ x e. X ) -> ( W = ( x prefix ( # ` W ) ) <-> x = ( W ++ <" v "> ) ) )
39 38 ralrimiva 
 |-  ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) -> A. x e. X ( W = ( x prefix ( # ` W ) ) <-> x = ( W ++ <" v "> ) ) )
40 reu6i 
 |-  ( ( ( W ++ <" v "> ) e. X /\ A. x e. X ( W = ( x prefix ( # ` W ) ) <-> x = ( W ++ <" v "> ) ) ) -> E! x e. X W = ( x prefix ( # ` W ) ) )
41 21 39 40 syl2anc 
 |-  ( ( ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) /\ v e. V ) /\ ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) ) -> E! x e. X W = ( x prefix ( # ` W ) ) )
42 41 exp31 
 |-  ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) -> ( v e. V -> ( ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) -> E! x e. X W = ( x prefix ( # ` W ) ) ) ) )
43 18 20 42 rexlimd 
 |-  ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) -> ( E. v e. V ( ( W ++ <" v "> ) e. X /\ A. u e. V ( ( W ++ <" u "> ) e. X -> v = u ) ) -> E! x e. X W = ( x prefix ( # ` W ) ) ) )
44 14 43 syl5bi 
 |-  ( ( W e. Word V /\ A. y e. X ( y e. Word V /\ ( # ` y ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix ( # ` W ) ) ) )
45 5 44 sylan2b 
 |-  ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ ( # ` x ) = ( ( # ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix ( # ` W ) ) ) )