Metamath Proof Explorer

Theorem efgred

Description: The reduced word that forms the base of the sequence in efgsval is uniquely determined, given the terminal point. (Contributed by Mario Carneiro, 28-Sep-2015)

Ref Expression
Hypotheses efgval.w 
|- W = ( _I ` Word ( I X. 2o ) )
efgval.r 
|- .~ = ( ~FG ` I )
efgval2.m 
|- M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
efgval2.t 
|- T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
efgred.d 
|- D = ( W \ U_ x e. W ran ( T ` x ) )
efgred.s 
|- S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
Assertion efgred 
|- ( ( A e. dom S /\ B e. dom S /\ ( S ` A ) = ( S ` B ) ) -> ( A ` 0 ) = ( B ` 0 ) )

Proof

Step Hyp Ref Expression
1 efgval.w 
 |-  W = ( _I ` Word ( I X. 2o ) )
2 efgval.r 
 |-  .~ = ( ~FG ` I )
3 efgval2.m 
 |-  M = ( y e. I , z e. 2o |-> <. y , ( 1o \ z ) >. )
4 efgval2.t 
 |-  T = ( v e. W |-> ( n e. ( 0 ... ( # ` v ) ) , w e. ( I X. 2o ) |-> ( v splice <. n , n , <" w ( M ` w ) "> >. ) ) )
5 efgred.d 
 |-  D = ( W \ U_ x e. W ran ( T ` x ) )
6 efgred.s 
 |-  S = ( m e. { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } |-> ( m ` ( ( # ` m ) - 1 ) ) )
7 fviss 
 |-  ( _I ` Word ( I X. 2o ) ) C_ Word ( I X. 2o )
8 1 7 eqsstri 
 |-  W C_ Word ( I X. 2o )
9 1 2 3 4 5 6 efgsf 
 |-  S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W
10 9 fdmi 
 |-  dom S = { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) }
11 10 feq2i 
 |-  ( S : dom S --> W <-> S : { t e. ( Word W \ { (/) } ) | ( ( t ` 0 ) e. D /\ A. k e. ( 1 ..^ ( # ` t ) ) ( t ` k ) e. ran ( T ` ( t ` ( k - 1 ) ) ) ) } --> W )
12 9 11 mpbir 
 |-  S : dom S --> W
13 12 ffvelrni 
 |-  ( A e. dom S -> ( S ` A ) e. W )
14 13 adantr 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( S ` A ) e. W )
15 8 14 sseldi 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( S ` A ) e. Word ( I X. 2o ) )
16 lencl 
 |-  ( ( S ` A ) e. Word ( I X. 2o ) -> ( # ` ( S ` A ) ) e. NN0 )
17 15 16 syl 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( # ` ( S ` A ) ) e. NN0 )
18 peano2nn0 
 |-  ( ( # ` ( S ` A ) ) e. NN0 -> ( ( # ` ( S ` A ) ) + 1 ) e. NN0 )
19 17 18 syl 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( ( # ` ( S ` A ) ) + 1 ) e. NN0 )
20 breq2 
 |-  ( c = 0 -> ( ( # ` ( S ` a ) ) < c <-> ( # ` ( S ` a ) ) < 0 ) )
21 20 imbi1d 
 |-  ( c = 0 -> ( ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < 0 -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
22 21 2ralbidv 
 |-  ( c = 0 -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < 0 -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
23 breq2 
 |-  ( c = i -> ( ( # ` ( S ` a ) ) < c <-> ( # ` ( S ` a ) ) < i ) )
24 23 imbi1d 
 |-  ( c = i -> ( ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
25 24 2ralbidv 
 |-  ( c = i -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
26 breq2 
 |-  ( c = ( i + 1 ) -> ( ( # ` ( S ` a ) ) < c <-> ( # ` ( S ` a ) ) < ( i + 1 ) ) )
27 26 imbi1d 
 |-  ( c = ( i + 1 ) -> ( ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
28 27 2ralbidv 
 |-  ( c = ( i + 1 ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
29 breq2 
 |-  ( c = ( ( # ` ( S ` A ) ) + 1 ) -> ( ( # ` ( S ` a ) ) < c <-> ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) ) )
30 29 imbi1d 
 |-  ( c = ( ( # ` ( S ` A ) ) + 1 ) -> ( ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
31 30 2ralbidv 
 |-  ( c = ( ( # ` ( S ` A ) ) + 1 ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < c -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
32 12 ffvelrni 
 |-  ( a e. dom S -> ( S ` a ) e. W )
33 8 32 sseldi 
 |-  ( a e. dom S -> ( S ` a ) e. Word ( I X. 2o ) )
34 lencl 
 |-  ( ( S ` a ) e. Word ( I X. 2o ) -> ( # ` ( S ` a ) ) e. NN0 )
35 33 34 syl 
 |-  ( a e. dom S -> ( # ` ( S ` a ) ) e. NN0 )
36 nn0nlt0 
 |-  ( ( # ` ( S ` a ) ) e. NN0 -> -. ( # ` ( S ` a ) ) < 0 )
37 35 36 syl 
 |-  ( a e. dom S -> -. ( # ` ( S ` a ) ) < 0 )
38 37 pm2.21d 
 |-  ( a e. dom S -> ( ( # ` ( S ` a ) ) < 0 -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
39 38 adantr 
 |-  ( ( a e. dom S /\ b e. dom S ) -> ( ( # ` ( S ` a ) ) < 0 -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
40 39 rgen2 
 |-  A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < 0 -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) )
41 simpl1 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
42 simpl3l 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> ( # ` ( S ` c ) ) = i )
43 breq2 
 |-  ( ( # ` ( S ` c ) ) = i -> ( ( # ` ( S ` a ) ) < ( # ` ( S ` c ) ) <-> ( # ` ( S ` a ) ) < i ) )
44 43 imbi1d 
 |-  ( ( # ` ( S ` c ) ) = i -> ( ( ( # ` ( S ` a ) ) < ( # ` ( S ` c ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
45 44 2ralbidv 
 |-  ( ( # ` ( S ` c ) ) = i -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` c ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
46 42 45 syl 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` c ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
47 41 46 mpbird 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( # ` ( S ` c ) ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
48 simpl2l 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> c e. dom S )
49 simpl2r 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> d e. dom S )
50 simpl3r 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> ( S ` c ) = ( S ` d ) )
51 simpr 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) -> -. ( c ` 0 ) = ( d ` 0 ) )
52 1 2 3 4 5 6 47 48 49 50 51 efgredlem 
 |-  -. ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) )
53 iman 
 |-  ( ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) -> ( c ` 0 ) = ( d ` 0 ) ) <-> -. ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) /\ -. ( c ` 0 ) = ( d ` 0 ) ) )
54 52 53 mpbir 
 |-  ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) /\ ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) ) -> ( c ` 0 ) = ( d ` 0 ) )
55 54 3expia 
 |-  ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) ) -> ( ( ( # ` ( S ` c ) ) = i /\ ( S ` c ) = ( S ` d ) ) -> ( c ` 0 ) = ( d ` 0 ) ) )
56 55 expd 
 |-  ( ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( c e. dom S /\ d e. dom S ) ) -> ( ( # ` ( S ` c ) ) = i -> ( ( S ` c ) = ( S ` d ) -> ( c ` 0 ) = ( d ` 0 ) ) ) )
57 56 ralrimivva 
 |-  ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) -> A. c e. dom S A. d e. dom S ( ( # ` ( S ` c ) ) = i -> ( ( S ` c ) = ( S ` d ) -> ( c ` 0 ) = ( d ` 0 ) ) ) )
58 2fveq3 
 |-  ( c = a -> ( # ` ( S ` c ) ) = ( # ` ( S ` a ) ) )
59 58 eqeq1d 
 |-  ( c = a -> ( ( # ` ( S ` c ) ) = i <-> ( # ` ( S ` a ) ) = i ) )
60 fveqeq2 
 |-  ( c = a -> ( ( S ` c ) = ( S ` d ) <-> ( S ` a ) = ( S ` d ) ) )
61 fveq1 
 |-  ( c = a -> ( c ` 0 ) = ( a ` 0 ) )
62 61 eqeq1d 
 |-  ( c = a -> ( ( c ` 0 ) = ( d ` 0 ) <-> ( a ` 0 ) = ( d ` 0 ) ) )
63 60 62 imbi12d 
 |-  ( c = a -> ( ( ( S ` c ) = ( S ` d ) -> ( c ` 0 ) = ( d ` 0 ) ) <-> ( ( S ` a ) = ( S ` d ) -> ( a ` 0 ) = ( d ` 0 ) ) ) )
64 59 63 imbi12d 
 |-  ( c = a -> ( ( ( # ` ( S ` c ) ) = i -> ( ( S ` c ) = ( S ` d ) -> ( c ` 0 ) = ( d ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` d ) -> ( a ` 0 ) = ( d ` 0 ) ) ) ) )
65 fveq2 
 |-  ( d = b -> ( S ` d ) = ( S ` b ) )
66 65 eqeq2d 
 |-  ( d = b -> ( ( S ` a ) = ( S ` d ) <-> ( S ` a ) = ( S ` b ) ) )
67 fveq1 
 |-  ( d = b -> ( d ` 0 ) = ( b ` 0 ) )
68 67 eqeq2d 
 |-  ( d = b -> ( ( a ` 0 ) = ( d ` 0 ) <-> ( a ` 0 ) = ( b ` 0 ) ) )
69 66 68 imbi12d 
 |-  ( d = b -> ( ( ( S ` a ) = ( S ` d ) -> ( a ` 0 ) = ( d ` 0 ) ) <-> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
70 69 imbi2d 
 |-  ( d = b -> ( ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` d ) -> ( a ` 0 ) = ( d ` 0 ) ) ) <-> ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
71 64 70 cbvral2vw 
 |-  ( A. c e. dom S A. d e. dom S ( ( # ` ( S ` c ) ) = i -> ( ( S ` c ) = ( S ` d ) -> ( c ` 0 ) = ( d ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
72 57 71 sylib 
 |-  ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
73 72 ancli 
 |-  ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
74 35 adantr 
 |-  ( ( a e. dom S /\ b e. dom S ) -> ( # ` ( S ` a ) ) e. NN0 )
75 nn0leltp1 
 |-  ( ( ( # ` ( S ` a ) ) e. NN0 /\ i e. NN0 ) -> ( ( # ` ( S ` a ) ) <_ i <-> ( # ` ( S ` a ) ) < ( i + 1 ) ) )
76 nn0re 
 |-  ( ( # ` ( S ` a ) ) e. NN0 -> ( # ` ( S ` a ) ) e. RR )
77 nn0re 
 |-  ( i e. NN0 -> i e. RR )
78 leloe 
 |-  ( ( ( # ` ( S ` a ) ) e. RR /\ i e. RR ) -> ( ( # ` ( S ` a ) ) <_ i <-> ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) ) )
79 76 77 78 syl2an 
 |-  ( ( ( # ` ( S ` a ) ) e. NN0 /\ i e. NN0 ) -> ( ( # ` ( S ` a ) ) <_ i <-> ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) ) )
80 75 79 bitr3d 
 |-  ( ( ( # ` ( S ` a ) ) e. NN0 /\ i e. NN0 ) -> ( ( # ` ( S ` a ) ) < ( i + 1 ) <-> ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) ) )
81 80 ancoms 
 |-  ( ( i e. NN0 /\ ( # ` ( S ` a ) ) e. NN0 ) -> ( ( # ` ( S ` a ) ) < ( i + 1 ) <-> ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) ) )
82 74 81 sylan2 
 |-  ( ( i e. NN0 /\ ( a e. dom S /\ b e. dom S ) ) -> ( ( # ` ( S ` a ) ) < ( i + 1 ) <-> ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) ) )
83 82 imbi1d 
 |-  ( ( i e. NN0 /\ ( a e. dom S /\ b e. dom S ) ) -> ( ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
84 jaob 
 |-  ( ( ( ( # ` ( S ` a ) ) < i \/ ( # ` ( S ` a ) ) = i ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
85 83 84 bitrdi 
 |-  ( ( i e. NN0 /\ ( a e. dom S /\ b e. dom S ) ) -> ( ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) ) )
86 85 2ralbidva 
 |-  ( i e. NN0 -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> A. a e. dom S A. b e. dom S ( ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) ) )
87 r19.26-2 
 |-  ( A. a e. dom S A. b e. dom S ( ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) <-> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
88 86 87 bitrdi 
 |-  ( i e. NN0 -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) /\ A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) = i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) ) )
89 73 88 syl5ibr 
 |-  ( i e. NN0 -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < i -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( i + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) ) )
90 22 25 28 31 40 89 nn0ind 
 |-  ( ( ( # ` ( S ` A ) ) + 1 ) e. NN0 -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
91 19 90 syl 
 |-  ( ( A e. dom S /\ B e. dom S ) -> A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) )
92 17 nn0red 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( # ` ( S ` A ) ) e. RR )
93 92 ltp1d 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( # ` ( S ` A ) ) < ( ( # ` ( S ` A ) ) + 1 ) )
94 2fveq3 
 |-  ( a = A -> ( # ` ( S ` a ) ) = ( # ` ( S ` A ) ) )
95 94 breq1d 
 |-  ( a = A -> ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) <-> ( # ` ( S ` A ) ) < ( ( # ` ( S ` A ) ) + 1 ) ) )
96 fveqeq2 
 |-  ( a = A -> ( ( S ` a ) = ( S ` b ) <-> ( S ` A ) = ( S ` b ) ) )
97 fveq1 
 |-  ( a = A -> ( a ` 0 ) = ( A ` 0 ) )
98 97 eqeq1d 
 |-  ( a = A -> ( ( a ` 0 ) = ( b ` 0 ) <-> ( A ` 0 ) = ( b ` 0 ) ) )
99 96 98 imbi12d 
 |-  ( a = A -> ( ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` A ) = ( S ` b ) -> ( A ` 0 ) = ( b ` 0 ) ) ) )
100 95 99 imbi12d 
 |-  ( a = A -> ( ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` A ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` A ) = ( S ` b ) -> ( A ` 0 ) = ( b ` 0 ) ) ) ) )
101 fveq2 
 |-  ( b = B -> ( S ` b ) = ( S ` B ) )
102 101 eqeq2d 
 |-  ( b = B -> ( ( S ` A ) = ( S ` b ) <-> ( S ` A ) = ( S ` B ) ) )
103 fveq1 
 |-  ( b = B -> ( b ` 0 ) = ( B ` 0 ) )
104 103 eqeq2d 
 |-  ( b = B -> ( ( A ` 0 ) = ( b ` 0 ) <-> ( A ` 0 ) = ( B ` 0 ) ) )
105 102 104 imbi12d 
 |-  ( b = B -> ( ( ( S ` A ) = ( S ` b ) -> ( A ` 0 ) = ( b ` 0 ) ) <-> ( ( S ` A ) = ( S ` B ) -> ( A ` 0 ) = ( B ` 0 ) ) ) )
106 105 imbi2d 
 |-  ( b = B -> ( ( ( # ` ( S ` A ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` A ) = ( S ` b ) -> ( A ` 0 ) = ( b ` 0 ) ) ) <-> ( ( # ` ( S ` A ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` A ) = ( S ` B ) -> ( A ` 0 ) = ( B ` 0 ) ) ) ) )
107 100 106 rspc2v 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( A. a e. dom S A. b e. dom S ( ( # ` ( S ` a ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` a ) = ( S ` b ) -> ( a ` 0 ) = ( b ` 0 ) ) ) -> ( ( # ` ( S ` A ) ) < ( ( # ` ( S ` A ) ) + 1 ) -> ( ( S ` A ) = ( S ` B ) -> ( A ` 0 ) = ( B ` 0 ) ) ) ) )
108 91 93 107 mp2d 
 |-  ( ( A e. dom S /\ B e. dom S ) -> ( ( S ` A ) = ( S ` B ) -> ( A ` 0 ) = ( B ` 0 ) ) )
109 108 3impia 
 |-  ( ( A e. dom S /\ B e. dom S /\ ( S ` A ) = ( S ` B ) ) -> ( A ` 0 ) = ( B ` 0 ) )