Metamath Proof Explorer

Theorem s3rex

Description: Membership in a family of words of length 3. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypothesis s3rex.1 
|- S e. _V
Assertion s3rex 
|- ( A e. ( S ^m ( 0 ..^ 3 ) ) <-> E. x e. S E. y e. S E. z e. S A = <" x y z "> )

Proof

Step Hyp Ref Expression
1 s3rex.1 
 |-  S e. _V
2 id 
 |-  ( x = ( A ` 0 ) -> x = ( A ` 0 ) )
3 eqidd 
 |-  ( x = ( A ` 0 ) -> y = y )
4 eqidd 
 |-  ( x = ( A ` 0 ) -> z = z )
5 2 3 4 s3eqd 
 |-  ( x = ( A ` 0 ) -> <" x y z "> = <" ( A ` 0 ) y z "> )
6 5 eqeq2d 
 |-  ( x = ( A ` 0 ) -> ( A = <" x y z "> <-> A = <" ( A ` 0 ) y z "> ) )
7 s3eq2 
 |-  ( y = ( A ` 1 ) -> <" ( A ` 0 ) y z "> = <" ( A ` 0 ) ( A ` 1 ) z "> )
8 7 eqeq2d 
 |-  ( y = ( A ` 1 ) -> ( A = <" ( A ` 0 ) y z "> <-> A = <" ( A ` 0 ) ( A ` 1 ) z "> ) )
9 eqidd 
 |-  ( z = ( A ` 2 ) -> ( A ` 0 ) = ( A ` 0 ) )
10 eqidd 
 |-  ( z = ( A ` 2 ) -> ( A ` 1 ) = ( A ` 1 ) )
11 id 
 |-  ( z = ( A ` 2 ) -> z = ( A ` 2 ) )
12 9 10 11 s3eqd 
 |-  ( z = ( A ` 2 ) -> <" ( A ` 0 ) ( A ` 1 ) z "> = <" ( A ` 0 ) ( A ` 1 ) ( A ` 2 ) "> )
13 12 eqeq2d 
 |-  ( z = ( A ` 2 ) -> ( A = <" ( A ` 0 ) ( A ` 1 ) z "> <-> A = <" ( A ` 0 ) ( A ` 1 ) ( A ` 2 ) "> ) )
14 elmapi 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> A : ( 0 ..^ 3 ) --> S )
15 c0ex 
 |-  0 e. _V
16 15 tpid1 
 |-  0 e. { 0 , 1 , 2 }
17 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
18 16 17 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
19 18 a1i 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> 0 e. ( 0 ..^ 3 ) )
20 14 19 ffvelcdmd 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> ( A ` 0 ) e. S )
21 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
22 21 17 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
23 22 a1i 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> 1 e. ( 0 ..^ 3 ) )
24 14 23 ffvelcdmd 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> ( A ` 1 ) e. S )
25 2ex 
 |-  2 e. _V
26 25 tpid3 
 |-  2 e. { 0 , 1 , 2 }
27 26 17 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
28 27 a1i 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> 2 e. ( 0 ..^ 3 ) )
29 14 28 ffvelcdmd 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> ( A ` 2 ) e. S )
30 iswrdi 
 |-  ( A : ( 0 ..^ 3 ) --> S -> A e. Word S )
31 14 30 syl 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> A e. Word S )
32 elmapfn 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> A Fn ( 0 ..^ 3 ) )
33 hashfn 
 |-  ( A Fn ( 0 ..^ 3 ) -> ( # ` A ) = ( # ` ( 0 ..^ 3 ) ) )
34 32 33 syl 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> ( # ` A ) = ( # ` ( 0 ..^ 3 ) ) )
35 3nn0 
 |-  3 e. NN0
36 hashfzo0 
 |-  ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
37 35 36 ax-mp 
 |-  ( # ` ( 0 ..^ 3 ) ) = 3
38 34 37 eqtrdi 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> ( # ` A ) = 3 )
39 wrdlen3s3 
 |-  ( ( A e. Word S /\ ( # ` A ) = 3 ) -> A = <" ( A ` 0 ) ( A ` 1 ) ( A ` 2 ) "> )
40 31 38 39 syl2anc 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> A = <" ( A ` 0 ) ( A ` 1 ) ( A ` 2 ) "> )
41 6 8 13 20 24 29 40 3rspcedvdw 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) -> E. x e. S E. y e. S E. z e. S A = <" x y z "> )
42 1 a1i 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> S e. _V )
43 ovexd 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> ( 0 ..^ 3 ) e. _V )
44 simpr 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> A = <" x y z "> )
45 44 fveq2d 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> ( # ` A ) = ( # ` <" x y z "> ) )
46 s3len 
 |-  ( # ` <" x y z "> ) = 3
47 45 46 eqtr2di 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> 3 = ( # ` A ) )
48 simplll 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> x e. S )
49 simpllr 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> y e. S )
50 simplr 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> z e. S )
51 48 49 50 s3cld 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> <" x y z "> e. Word S )
52 44 51 eqeltrd 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> A e. Word S )
53 47 52 wrdfd 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> A : ( 0 ..^ 3 ) --> S )
54 42 43 53 elmapdd 
 |-  ( ( ( ( x e. S /\ y e. S ) /\ z e. S ) /\ A = <" x y z "> ) -> A e. ( S ^m ( 0 ..^ 3 ) ) )
55 54 rexlimdva2 
 |-  ( ( x e. S /\ y e. S ) -> ( E. z e. S A = <" x y z "> -> A e. ( S ^m ( 0 ..^ 3 ) ) ) )
56 55 rexlimivv 
 |-  ( E. x e. S E. y e. S E. z e. S A = <" x y z "> -> A e. ( S ^m ( 0 ..^ 3 ) ) )
57 41 56 impbii 
 |-  ( A e. ( S ^m ( 0 ..^ 3 ) ) <-> E. x e. S E. y e. S E. z e. S A = <" x y z "> )