Metamath Proof Explorer

Theorem tocyccntz

Description: All elements of a (finite) set of cycles commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 27-Nov-2023)

Ref Expression
Hypotheses tocyccntz.s 
|- S = ( SymGrp ` D )
tocyccntz.z 
|- Z = ( Cntz ` S )
tocyccntz.m 
|- M = ( toCyc ` D )
tocyccntz.1 
|- ( ph -> D e. V )
tocyccntz.2 
|- ( ph -> Disj_ x e. A ran x )
tocyccntz.a 
|- ( ph -> A C_ dom M )
Assertion tocyccntz 
|- ( ph -> ( M " A ) C_ ( Z ` ( M " A ) ) )

Proof

Step Hyp Ref Expression
1 tocyccntz.s 
 |-  S = ( SymGrp ` D )
2 tocyccntz.z 
 |-  Z = ( Cntz ` S )
3 tocyccntz.m 
 |-  M = ( toCyc ` D )
4 tocyccntz.1 
 |-  ( ph -> D e. V )
5 tocyccntz.2 
 |-  ( ph -> Disj_ x e. A ran x )
6 tocyccntz.a 
 |-  ( ph -> A C_ dom M )
7 eqid 
 |-  ( Base ` S ) = ( Base ` S )
8 3 1 7 tocycf 
 |-  ( D e. V -> M : { c e. Word D | c : dom c -1-1-> D } --> ( Base ` S ) )
9 fimass 
 |-  ( M : { c e. Word D | c : dom c -1-1-> D } --> ( Base ` S ) -> ( M " A ) C_ ( Base ` S ) )
10 4 8 9 3syl 
 |-  ( ph -> ( M " A ) C_ ( Base ` S ) )
11 difss 
 |-  ( A \ ( `' # " { 0 , 1 } ) ) C_ A
12 disjss1 
 |-  ( ( A \ ( `' # " { 0 , 1 } ) ) C_ A -> ( Disj_ x e. A ran x -> Disj_ x e. ( A \ ( `' # " { 0 , 1 } ) ) ran x ) )
13 11 5 12 mpsyl 
 |-  ( ph -> Disj_ x e. ( A \ ( `' # " { 0 , 1 } ) ) ran x )
14 4 adantr 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> D e. V )
15 6 adantr 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> A C_ dom M )
16 simpr 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> x e. ( A \ ( `' # " { 0 , 1 } ) ) )
17 16 eldifad 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> x e. A )
18 15 17 sseldd 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> x e. dom M )
19 fdm 
 |-  ( M : { c e. Word D | c : dom c -1-1-> D } --> ( Base ` S ) -> dom M = { c e. Word D | c : dom c -1-1-> D } )
20 14 8 19 3syl 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> dom M = { c e. Word D | c : dom c -1-1-> D } )
21 18 20 eleqtrd 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> x e. { c e. Word D | c : dom c -1-1-> D } )
22 id 
 |-  ( c = x -> c = x )
23 dmeq 
 |-  ( c = x -> dom c = dom x )
24 eqidd 
 |-  ( c = x -> D = D )
25 22 23 24 f1eq123d 
 |-  ( c = x -> ( c : dom c -1-1-> D <-> x : dom x -1-1-> D ) )
26 25 elrab 
 |-  ( x e. { c e. Word D | c : dom c -1-1-> D } <-> ( x e. Word D /\ x : dom x -1-1-> D ) )
27 21 26 sylib 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> ( x e. Word D /\ x : dom x -1-1-> D ) )
28 27 simpld 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> x e. Word D )
29 27 simprd 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> x : dom x -1-1-> D )
30 16 eldifbd 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> -. x e. ( `' # " { 0 , 1 } ) )
31 hashgt1 
 |-  ( x e. _V -> ( -. x e. ( `' # " { 0 , 1 } ) <-> 1 < ( # ` x ) ) )
32 31 elv 
 |-  ( -. x e. ( `' # " { 0 , 1 } ) <-> 1 < ( # ` x ) )
33 30 32 sylib 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> 1 < ( # ` x ) )
34 3 14 28 29 33 cycpmrn 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> ran x = dom ( ( M ` x ) \ _I ) )
35 16 fvresd 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) = ( M ` x ) )
36 35 difeq1d 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) = ( ( M ` x ) \ _I ) )
37 36 dmeqd 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> dom ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) = dom ( ( M ` x ) \ _I ) )
38 34 37 eqtr4d 
 |-  ( ( ph /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> ran x = dom ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) )
39 38 disjeq2dv 
 |-  ( ph -> ( Disj_ x e. ( A \ ( `' # " { 0 , 1 } ) ) ran x <-> Disj_ x e. ( A \ ( `' # " { 0 , 1 } ) ) dom ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) ) )
40 13 39 mpbid 
 |-  ( ph -> Disj_ x e. ( A \ ( `' # " { 0 , 1 } ) ) dom ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) )
41 4 8 syl 
 |-  ( ph -> M : { c e. Word D | c : dom c -1-1-> D } --> ( Base ` S ) )
42 41 ffdmd 
 |-  ( ph -> M : dom M --> ( Base ` S ) )
43 6 ssdifssd 
 |-  ( ph -> ( A \ ( `' # " { 0 , 1 } ) ) C_ dom M )
44 42 43 fssresd 
 |-  ( ph -> ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) --> ( Base ` S ) )
45 41 6 fssdmd 
 |-  ( ph -> A C_ { c e. Word D | c : dom c -1-1-> D } )
46 45 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> A C_ { c e. Word D | c : dom c -1-1-> D } )
47 simp-4r 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s e. ( A \ ( `' # " { 0 , 1 } ) ) )
48 47 eldifad 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s e. A )
49 46 48 sseldd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s e. { c e. Word D | c : dom c -1-1-> D } )
50 id 
 |-  ( c = s -> c = s )
51 dmeq 
 |-  ( c = s -> dom c = dom s )
52 eqidd 
 |-  ( c = s -> D = D )
53 50 51 52 f1eq123d 
 |-  ( c = s -> ( c : dom c -1-1-> D <-> s : dom s -1-1-> D ) )
54 53 elrab 
 |-  ( s e. { c e. Word D | c : dom c -1-1-> D } <-> ( s e. Word D /\ s : dom s -1-1-> D ) )
55 49 54 sylib 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( s e. Word D /\ s : dom s -1-1-> D ) )
56 55 simpld 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s e. Word D )
57 wrdf 
 |-  ( s e. Word D -> s : ( 0 ..^ ( # ` s ) ) --> D )
58 frel 
 |-  ( s : ( 0 ..^ ( # ` s ) ) --> D -> Rel s )
59 56 57 58 3syl 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> Rel s )
60 simplr 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) )
61 47 fvresd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( M ` s ) )
62 16 ad5ant13 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x e. ( A \ ( `' # " { 0 , 1 } ) ) )
63 62 fvresd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) = ( M ` x ) )
64 60 61 63 3eqtr3rd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( M ` x ) = ( M ` s ) )
65 64 difeq1d 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ( M ` x ) \ _I ) = ( ( M ` s ) \ _I ) )
66 65 dmeqd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> dom ( ( M ` x ) \ _I ) = dom ( ( M ` s ) \ _I ) )
67 4 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> D e. V )
68 17 ad5ant13 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x e. A )
69 46 68 sseldd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x e. { c e. Word D | c : dom c -1-1-> D } )
70 69 26 sylib 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( x e. Word D /\ x : dom x -1-1-> D ) )
71 70 simpld 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x e. Word D )
72 70 simprd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x : dom x -1-1-> D )
73 33 ad5ant13 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> 1 < ( # ` x ) )
74 3 67 71 72 73 cycpmrn 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ran x = dom ( ( M ` x ) \ _I ) )
75 55 simprd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s : dom s -1-1-> D )
76 6 ssdifd 
 |-  ( ph -> ( A \ ( `' # " { 0 , 1 } ) ) C_ ( dom M \ ( `' # " { 0 , 1 } ) ) )
77 76 sselda 
 |-  ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> s e. ( dom M \ ( `' # " { 0 , 1 } ) ) )
78 77 ad3antrrr 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s e. ( dom M \ ( `' # " { 0 , 1 } ) ) )
79 78 eldifbd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> -. s e. ( `' # " { 0 , 1 } ) )
80 hashgt1 
 |-  ( s e. A -> ( -. s e. ( `' # " { 0 , 1 } ) <-> 1 < ( # ` s ) ) )
81 80 biimpa 
 |-  ( ( s e. A /\ -. s e. ( `' # " { 0 , 1 } ) ) -> 1 < ( # ` s ) )
82 48 79 81 syl2anc 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> 1 < ( # ` s ) )
83 3 67 56 75 82 cycpmrn 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ran s = dom ( ( M ` s ) \ _I ) )
84 66 74 83 3eqtr4rd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ran s = ran x )
85 84 ineq2d 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ran x i^i ran s ) = ( ran x i^i ran x ) )
86 inidm 
 |-  ( ran x i^i ran x ) = ran x
87 85 86 eqtrdi 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ran x i^i ran s ) = ran x )
88 rneq 
 |-  ( x = y -> ran x = ran y )
89 88 cbvdisjv 
 |-  ( Disj_ x e. A ran x <-> Disj_ y e. A ran y )
90 5 89 sylib 
 |-  ( ph -> Disj_ y e. A ran y )
91 90 ad4antr 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> Disj_ y e. A ran y )
92 simpr 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> -. s = x )
93 92 neqned 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s =/= x )
94 93 necomd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x =/= s )
95 rneq 
 |-  ( y = x -> ran y = ran x )
96 rneq 
 |-  ( y = s -> ran y = ran s )
97 95 96 disji2 
 |-  ( ( Disj_ y e. A ran y /\ ( x e. A /\ s e. A ) /\ x =/= s ) -> ( ran x i^i ran s ) = (/) )
98 91 68 48 94 97 syl121anc 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ( ran x i^i ran s ) = (/) )
99 87 98 eqtr3d 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ran x = (/) )
100 84 99 eqtrd 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> ran s = (/) )
101 relrn0 
 |-  ( Rel s -> ( s = (/) <-> ran s = (/) ) )
102 101 biimpar 
 |-  ( ( Rel s /\ ran s = (/) ) -> s = (/) )
103 59 100 102 syl2anc 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s = (/) )
104 wrdf 
 |-  ( x e. Word D -> x : ( 0 ..^ ( # ` x ) ) --> D )
105 frel 
 |-  ( x : ( 0 ..^ ( # ` x ) ) --> D -> Rel x )
106 71 104 105 3syl 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> Rel x )
107 relrn0 
 |-  ( Rel x -> ( x = (/) <-> ran x = (/) ) )
108 107 biimpar 
 |-  ( ( Rel x /\ ran x = (/) ) -> x = (/) )
109 106 99 108 syl2anc 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> x = (/) )
110 103 109 eqtr4d 
 |-  ( ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) /\ -. s = x ) -> s = x )
111 110 pm2.18da 
 |-  ( ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) -> s = x )
112 111 ex 
 |-  ( ( ( ph /\ s e. ( A \ ( `' # " { 0 , 1 } ) ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) -> ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) -> s = x ) )
113 112 anasss 
 |-  ( ( ph /\ ( s e. ( A \ ( `' # " { 0 , 1 } ) ) /\ x e. ( A \ ( `' # " { 0 , 1 } ) ) ) ) -> ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) -> s = x ) )
114 113 ralrimivva 
 |-  ( ph -> A. s e. ( A \ ( `' # " { 0 , 1 } ) ) A. x e. ( A \ ( `' # " { 0 , 1 } ) ) ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) -> s = x ) )
115 dff13 
 |-  ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-> ( Base ` S ) <-> ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) --> ( Base ` S ) /\ A. s e. ( A \ ( `' # " { 0 , 1 } ) ) A. x e. ( A \ ( `' # " { 0 , 1 } ) ) ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` s ) = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) -> s = x ) ) )
116 44 114 115 sylanbrc 
 |-  ( ph -> ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-> ( Base ` S ) )
117 f1f1orn 
 |-  ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-> ( Base ` S ) -> ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-onto-> ran ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) )
118 116 117 syl 
 |-  ( ph -> ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-onto-> ran ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) )
119 df-ima 
 |-  ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) = ran ( M |` ( A \ ( `' # " { 0 , 1 } ) ) )
120 119 a1i 
 |-  ( ph -> ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) = ran ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) )
121 120 f1oeq3d 
 |-  ( ph -> ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-onto-> ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) <-> ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-onto-> ran ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ) )
122 118 121 mpbird 
 |-  ( ph -> ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) : ( A \ ( `' # " { 0 , 1 } ) ) -1-1-onto-> ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) )
123 simpr 
 |-  ( ( ph /\ c = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) -> c = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) )
124 123 difeq1d 
 |-  ( ( ph /\ c = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) -> ( c \ _I ) = ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) )
125 124 dmeqd 
 |-  ( ( ph /\ c = ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) ) -> dom ( c \ _I ) = dom ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) )
126 122 125 disjrdx 
 |-  ( ph -> ( Disj_ x e. ( A \ ( `' # " { 0 , 1 } ) ) dom ( ( ( M |` ( A \ ( `' # " { 0 , 1 } ) ) ) ` x ) \ _I ) <-> Disj_ c e. ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) dom ( c \ _I ) ) )
127 40 126 mpbid 
 |-  ( ph -> Disj_ c e. ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) dom ( c \ _I ) )
128 simpr 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> ( M ` x ) = c )
129 4 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> D e. V )
130 6 ssrind 
 |-  ( ph -> ( A i^i ( `' # " { 0 , 1 } ) ) C_ ( dom M i^i ( `' # " { 0 , 1 } ) ) )
131 130 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> ( A i^i ( `' # " { 0 , 1 } ) ) C_ ( dom M i^i ( `' # " { 0 , 1 } ) ) )
132 simplr 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> x e. ( A i^i ( `' # " { 0 , 1 } ) ) )
133 131 132 sseldd 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> x e. ( dom M i^i ( `' # " { 0 , 1 } ) ) )
134 3 tocyc01 
 |-  ( ( D e. V /\ x e. ( dom M i^i ( `' # " { 0 , 1 } ) ) ) -> ( M ` x ) = ( _I |` D ) )
135 129 133 134 syl2anc 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> ( M ` x ) = ( _I |` D ) )
136 128 135 eqtr3d 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> c = ( _I |` D ) )
137 136 difeq1d 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> ( c \ _I ) = ( ( _I |` D ) \ _I ) )
138 137 dmeqd 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> dom ( c \ _I ) = dom ( ( _I |` D ) \ _I ) )
139 resdifcom 
 |-  ( ( _I |` D ) \ _I ) = ( ( _I \ _I ) |` D )
140 difid 
 |-  ( _I \ _I ) = (/)
141 140 reseq1i 
 |-  ( ( _I \ _I ) |` D ) = ( (/) |` D )
142 0res 
 |-  ( (/) |` D ) = (/)
143 139 141 142 3eqtri 
 |-  ( ( _I |` D ) \ _I ) = (/)
144 143 dmeqi 
 |-  dom ( ( _I |` D ) \ _I ) = dom (/)
145 dm0 
 |-  dom (/) = (/)
146 144 145 eqtri 
 |-  dom ( ( _I |` D ) \ _I ) = (/)
147 138 146 eqtrdi 
 |-  ( ( ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) /\ x e. ( A i^i ( `' # " { 0 , 1 } ) ) ) /\ ( M ` x ) = c ) -> dom ( c \ _I ) = (/) )
148 41 ffund 
 |-  ( ph -> Fun M )
149 fvelima 
 |-  ( ( Fun M /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) -> E. x e. ( A i^i ( `' # " { 0 , 1 } ) ) ( M ` x ) = c )
150 148 149 sylan 
 |-  ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) -> E. x e. ( A i^i ( `' # " { 0 , 1 } ) ) ( M ` x ) = c )
151 147 150 r19.29a 
 |-  ( ( ph /\ c e. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) -> dom ( c \ _I ) = (/) )
152 151 disjxun0 
 |-  ( ph -> ( Disj_ c e. ( ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) dom ( c \ _I ) <-> Disj_ c e. ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) dom ( c \ _I ) ) )
153 127 152 mpbird 
 |-  ( ph -> Disj_ c e. ( ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) dom ( c \ _I ) )
154 uncom 
 |-  ( ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) = ( ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) )
155 imaundi 
 |-  ( M " ( ( A i^i ( `' # " { 0 , 1 } ) ) u. ( A \ ( `' # " { 0 , 1 } ) ) ) ) = ( ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) )
156 inundif 
 |-  ( ( A i^i ( `' # " { 0 , 1 } ) ) u. ( A \ ( `' # " { 0 , 1 } ) ) ) = A
157 156 imaeq2i 
 |-  ( M " ( ( A i^i ( `' # " { 0 , 1 } ) ) u. ( A \ ( `' # " { 0 , 1 } ) ) ) ) = ( M " A )
158 154 155 157 3eqtr2i 
 |-  ( ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) = ( M " A )
159 158 a1i 
 |-  ( ph -> ( ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) = ( M " A ) )
160 159 disjeq1d 
 |-  ( ph -> ( Disj_ c e. ( ( M " ( A \ ( `' # " { 0 , 1 } ) ) ) u. ( M " ( A i^i ( `' # " { 0 , 1 } ) ) ) ) dom ( c \ _I ) <-> Disj_ c e. ( M " A ) dom ( c \ _I ) ) )
161 153 160 mpbid 
 |-  ( ph -> Disj_ c e. ( M " A ) dom ( c \ _I ) )
162 1 7 2 10 161 symgcntz 
 |-  ( ph -> ( M " A ) C_ ( Z ` ( M " A ) ) )