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	ffvelcdmi	\|- ( 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	sselid	\|- ( ( 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	ffvelcdmi	\|- ( a e. dom S -> ( S ` a ) e. W )
33	8 32	sselid	\|- ( 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	imbitrrid	\|- ( 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 ) )

Metamath Proof Explorer

Theorem efgred

Proof