Metamath Proof Explorer

Theorem poimirlem25

Description: Lemma for poimir stating that for a given simplex such that no vertex maps to N , the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020)

Ref Expression
Hypotheses poimir.0 
|- ( ph -> N e. NN )
poimirlem28.1 
|- ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
poimirlem28.2 
|- ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
poimirlem25.3 
|- ( ph -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
poimirlem25.4 
|- ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem25.5 
|- ( ( ph /\ j e. ( 0 ... N ) ) -> N =/= [_ <. T , U >. / s ]_ C )
Assertion poimirlem25 
|- ( ph -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )

Proof

Step Hyp Ref Expression
1 poimir.0 
 |-  ( ph -> N e. NN )
2 poimirlem28.1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> B = C )
3 poimirlem28.2 
 |-  ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) )
4 poimirlem25.3 
 |-  ( ph -> T : ( 1 ... N ) --> ( 0 ..^ K ) )
5 poimirlem25.4 
 |-  ( ph -> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
6 poimirlem25.5 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> N =/= [_ <. T , U >. / s ]_ C )
7 neq0 
 |-  ( -. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } = (/) <-> E. t t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } )
8 2z 
 |-  2 e. ZZ
9 iddvds 
 |-  ( 2 e. ZZ -> 2 || 2 )
10 8 9 ax-mp 
 |-  2 || 2
11 df-2 
 |-  2 = ( 1 + 1 )
12 10 11 breqtri 
 |-  2 || ( 1 + 1 )
13 vex 
 |-  t e. _V
14 fzfi 
 |-  ( 0 ... N ) e. Fin
15 rabfi 
 |-  ( ( 0 ... N ) e. Fin -> { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } e. Fin )
16 14 15 ax-mp 
 |-  { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } e. Fin
17 diffi 
 |-  ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } e. Fin -> ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) e. Fin )
18 16 17 ax-mp 
 |-  ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) e. Fin
19 neldifsn 
 |-  -. t e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } )
20 18 19 pm3.2i 
 |-  ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) e. Fin /\ -. t e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) )
21 hashunsng 
 |-  ( t e. _V -> ( ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) e. Fin /\ -. t e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) -> ( # ` ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) u. { t } ) ) = ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) + 1 ) ) )
22 13 20 21 mp2 
 |-  ( # ` ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) u. { t } ) ) = ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) + 1 )
23 difsnid 
 |-  ( t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } -> ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) u. { t } ) = { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } )
24 23 fveq2d 
 |-  ( t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } -> ( # ` ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) u. { t } ) ) = ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )
25 22 24 eqtr3id 
 |-  ( t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } -> ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) + 1 ) = ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )
26 25 adantl 
 |-  ( ( ph /\ t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) -> ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) + 1 ) = ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )
27 sneq 
 |-  ( y = t -> { y } = { t } )
28 27 difeq2d 
 |-  ( y = t -> ( ( 0 ... N ) \ { y } ) = ( ( 0 ... N ) \ { t } ) )
29 28 rexeqdv 
 |-  ( y = t -> ( E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
30 29 ralbidv 
 |-  ( y = t -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
31 30 elrab 
 |-  ( t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } <-> ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
32 6 ralrimiva 
 |-  ( ph -> A. j e. ( 0 ... N ) N =/= [_ <. T , U >. / s ]_ C )
33 nfcv 
 |-  F/_ j N
34 nfcsb1v 
 |-  F/_ j [_ t / j ]_ [_ <. T , U >. / s ]_ C
35 33 34 nfne 
 |-  F/ j N =/= [_ t / j ]_ [_ <. T , U >. / s ]_ C
36 csbeq1a 
 |-  ( j = t -> [_ <. T , U >. / s ]_ C = [_ t / j ]_ [_ <. T , U >. / s ]_ C )
37 36 neeq2d 
 |-  ( j = t -> ( N =/= [_ <. T , U >. / s ]_ C <-> N =/= [_ t / j ]_ [_ <. T , U >. / s ]_ C ) )
38 35 37 rspc 
 |-  ( t e. ( 0 ... N ) -> ( A. j e. ( 0 ... N ) N =/= [_ <. T , U >. / s ]_ C -> N =/= [_ t / j ]_ [_ <. T , U >. / s ]_ C ) )
39 32 38 mpan9 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> N =/= [_ t / j ]_ [_ <. T , U >. / s ]_ C )
40 nesym 
 |-  ( N =/= [_ t / j ]_ [_ <. T , U >. / s ]_ C <-> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = N )
41 39 40 sylib 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = N )
42 nfv 
 |-  F/ j ( ph /\ t e. ( 0 ... N ) )
43 34 nfel1 
 |-  F/ j [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N )
44 42 43 nfim 
 |-  F/ j ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) )
45 eleq1w 
 |-  ( j = t -> ( j e. ( 0 ... N ) <-> t e. ( 0 ... N ) ) )
46 45 anbi2d 
 |-  ( j = t -> ( ( ph /\ j e. ( 0 ... N ) ) <-> ( ph /\ t e. ( 0 ... N ) ) ) )
47 36 eleq1d 
 |-  ( j = t -> ( [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) ) )
48 46 47 imbi12d 
 |-  ( j = t -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... N ) ) <-> ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) ) ) )
49 ovex 
 |-  ( 0 ..^ K ) e. _V
50 ovex 
 |-  ( 1 ... N ) e. _V
51 49 50 elmap 
 |-  ( T e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) <-> T : ( 1 ... N ) --> ( 0 ..^ K ) )
52 4 51 sylibr 
 |-  ( ph -> T e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
53 fzfi 
 |-  ( 1 ... N ) e. Fin
54 f1oexrnex 
 |-  ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( 1 ... N ) e. Fin ) -> U e. _V )
55 53 54 mpan2 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U e. _V )
56 f1oeq1 
 |-  ( f = U -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
57 56 elabg 
 |-  ( U e. _V -> ( U e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
58 55 57 syl 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( U e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
59 58 ibir 
 |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> U e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
60 5 59 syl 
 |-  ( ph -> U e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
61 opelxpi 
 |-  ( ( T e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) /\ U e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> <. T , U >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
62 52 60 61 syl2anc 
 |-  ( ph -> <. T , U >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
63 62 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> <. T , U >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
64 nfcv 
 |-  F/_ s <. T , U >.
65 nfv 
 |-  F/ s ( ph /\ j e. ( 0 ... N ) )
66 nfcsb1v 
 |-  F/_ s [_ <. T , U >. / s ]_ C
67 66 nfel1 
 |-  F/ s [_ <. T , U >. / s ]_ C e. ( 0 ... N )
68 65 67 nfim 
 |-  F/ s ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... N ) )
69 csbeq1a 
 |-  ( s = <. T , U >. -> C = [_ <. T , U >. / s ]_ C )
70 69 eleq1d 
 |-  ( s = <. T , U >. -> ( C e. ( 0 ... N ) <-> [_ <. T , U >. / s ]_ C e. ( 0 ... N ) ) )
71 70 imbi2d 
 |-  ( s = <. T , U >. -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> C e. ( 0 ... N ) ) <-> ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... N ) ) ) )
72 elun 
 |-  ( p e. ( { 1 } u. { 0 } ) <-> ( p e. { 1 } \/ p e. { 0 } ) )
73 fzofzp1 
 |-  ( i e. ( 0 ..^ K ) -> ( i + 1 ) e. ( 0 ... K ) )
74 elsni 
 |-  ( p e. { 1 } -> p = 1 )
75 74 oveq2d 
 |-  ( p e. { 1 } -> ( i + p ) = ( i + 1 ) )
76 75 eleq1d 
 |-  ( p e. { 1 } -> ( ( i + p ) e. ( 0 ... K ) <-> ( i + 1 ) e. ( 0 ... K ) ) )
77 73 76 syl5ibrcom 
 |-  ( i e. ( 0 ..^ K ) -> ( p e. { 1 } -> ( i + p ) e. ( 0 ... K ) ) )
78 elfzonn0 
 |-  ( i e. ( 0 ..^ K ) -> i e. NN0 )
79 78 nn0cnd 
 |-  ( i e. ( 0 ..^ K ) -> i e. CC )
80 79 addid1d 
 |-  ( i e. ( 0 ..^ K ) -> ( i + 0 ) = i )
81 elfzofz 
 |-  ( i e. ( 0 ..^ K ) -> i e. ( 0 ... K ) )
82 80 81 eqeltrd 
 |-  ( i e. ( 0 ..^ K ) -> ( i + 0 ) e. ( 0 ... K ) )
83 elsni 
 |-  ( p e. { 0 } -> p = 0 )
84 83 oveq2d 
 |-  ( p e. { 0 } -> ( i + p ) = ( i + 0 ) )
85 84 eleq1d 
 |-  ( p e. { 0 } -> ( ( i + p ) e. ( 0 ... K ) <-> ( i + 0 ) e. ( 0 ... K ) ) )
86 82 85 syl5ibrcom 
 |-  ( i e. ( 0 ..^ K ) -> ( p e. { 0 } -> ( i + p ) e. ( 0 ... K ) ) )
87 77 86 jaod 
 |-  ( i e. ( 0 ..^ K ) -> ( ( p e. { 1 } \/ p e. { 0 } ) -> ( i + p ) e. ( 0 ... K ) ) )
88 72 87 syl5bi 
 |-  ( i e. ( 0 ..^ K ) -> ( p e. ( { 1 } u. { 0 } ) -> ( i + p ) e. ( 0 ... K ) ) )
89 88 imp 
 |-  ( ( i e. ( 0 ..^ K ) /\ p e. ( { 1 } u. { 0 } ) ) -> ( i + p ) e. ( 0 ... K ) )
90 89 adantl 
 |-  ( ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ j e. ( 0 ... N ) ) /\ ( i e. ( 0 ..^ K ) /\ p e. ( { 1 } u. { 0 } ) ) ) -> ( i + p ) e. ( 0 ... K ) )
91 xp1st 
 |-  ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` s ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
92 elmapi 
 |-  ( ( 1st ` s ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` s ) : ( 1 ... N ) --> ( 0 ..^ K ) )
93 91 92 syl 
 |-  ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` s ) : ( 1 ... N ) --> ( 0 ..^ K ) )
94 93 adantr 
 |-  ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ j e. ( 0 ... N ) ) -> ( 1st ` s ) : ( 1 ... N ) --> ( 0 ..^ K ) )
95 xp2nd 
 |-  ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` s ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
96 fvex 
 |-  ( 2nd ` s ) e. _V
97 f1oeq1 
 |-  ( f = ( 2nd ` s ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
98 96 97 elab 
 |-  ( ( 2nd ` s ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
99 95 98 sylib 
 |-  ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
100 1ex 
 |-  1 e. _V
101 100 fconst 
 |-  ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` s ) " ( 1 ... j ) ) --> { 1 }
102 c0ex 
 |-  0 e. _V
103 102 fconst 
 |-  ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) --> { 0 }
104 101 103 pm3.2i 
 |-  ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` s ) " ( 1 ... j ) ) --> { 1 } /\ ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) --> { 0 } )
105 dff1o3 
 |-  ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` s ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` s ) ) )
106 imain 
 |-  ( Fun `' ( 2nd ` s ) -> ( ( 2nd ` s ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` s ) " ( 1 ... j ) ) i^i ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) )
107 105 106 simplbiim 
 |-  ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( ( 2nd ` s ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` s ) " ( 1 ... j ) ) i^i ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) )
108 elfznn0 
 |-  ( j e. ( 0 ... N ) -> j e. NN0 )
109 108 nn0red 
 |-  ( j e. ( 0 ... N ) -> j e. RR )
110 109 ltp1d 
 |-  ( j e. ( 0 ... N ) -> j < ( j + 1 ) )
111 fzdisj 
 |-  ( j < ( j + 1 ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
112 110 111 syl 
 |-  ( j e. ( 0 ... N ) -> ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) = (/) )
113 112 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` s ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = ( ( 2nd ` s ) " (/) ) )
114 ima0 
 |-  ( ( 2nd ` s ) " (/) ) = (/)
115 113 114 eqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` s ) " ( ( 1 ... j ) i^i ( ( j + 1 ) ... N ) ) ) = (/) )
116 107 115 sylan9req 
 |-  ( ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ j e. ( 0 ... N ) ) -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) i^i ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) = (/) )
117 fun 
 |-  ( ( ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) : ( ( 2nd ` s ) " ( 1 ... j ) ) --> { 1 } /\ ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) : ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) --> { 0 } ) /\ ( ( ( 2nd ` s ) " ( 1 ... j ) ) i^i ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( 2nd ` s ) " ( 1 ... j ) ) u. ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
118 104 116 117 sylancr 
 |-  ( ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( 2nd ` s ) " ( 1 ... j ) ) u. ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
119 nn0p1nn 
 |-  ( j e. NN0 -> ( j + 1 ) e. NN )
120 108 119 syl 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. NN )
121 nnuz 
 |-  NN = ( ZZ>= ` 1 )
122 120 121 eleqtrdi 
 |-  ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( ZZ>= ` 1 ) )
123 elfzuz3 
 |-  ( j e. ( 0 ... N ) -> N e. ( ZZ>= ` j ) )
124 fzsplit2 
 |-  ( ( ( j + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` j ) ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
125 122 123 124 syl2anc 
 |-  ( j e. ( 0 ... N ) -> ( 1 ... N ) = ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) )
126 125 imaeq2d 
 |-  ( j e. ( 0 ... N ) -> ( ( 2nd ` s ) " ( 1 ... N ) ) = ( ( 2nd ` s ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) )
127 imaundi 
 |-  ( ( 2nd ` s ) " ( ( 1 ... j ) u. ( ( j + 1 ) ... N ) ) ) = ( ( ( 2nd ` s ) " ( 1 ... j ) ) u. ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) )
128 126 127 eqtr2di 
 |-  ( j e. ( 0 ... N ) -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) u. ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) = ( ( 2nd ` s ) " ( 1 ... N ) ) )
129 f1ofo 
 |-  ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` s ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
130 foima 
 |-  ( ( 2nd ` s ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` s ) " ( 1 ... N ) ) = ( 1 ... N ) )
131 129 130 syl 
 |-  ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( ( 2nd ` s ) " ( 1 ... N ) ) = ( 1 ... N ) )
132 128 131 sylan9eqr 
 |-  ( ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ j e. ( 0 ... N ) ) -> ( ( ( 2nd ` s ) " ( 1 ... j ) ) u. ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) = ( 1 ... N ) )
133 132 feq2d 
 |-  ( ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( 2nd ` s ) " ( 1 ... j ) ) u. ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) <-> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) ) )
134 118 133 mpbid 
 |-  ( ( ( 2nd ` s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
135 99 134 sylan 
 |-  ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ j e. ( 0 ... N ) ) -> ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
136 fzfid 
 |-  ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ j e. ( 0 ... N ) ) -> ( 1 ... N ) e. Fin )
137 inidm 
 |-  ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
138 90 94 135 136 136 137 off 
 |-  ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ j e. ( 0 ... N ) ) -> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) )
139 ovex 
 |-  ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
140 feq1 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( p : ( 1 ... N ) --> ( 0 ... K ) <-> ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) )
141 140 anbi2d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) <-> ( ph /\ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) ) )
142 2 eleq1d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( B e. ( 0 ... N ) <-> C e. ( 0 ... N ) ) )
143 141 142 imbi12d 
 |-  ( p = ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( ( ( ph /\ p : ( 1 ... N ) --> ( 0 ... K ) ) -> B e. ( 0 ... N ) ) <-> ( ( ph /\ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> C e. ( 0 ... N ) ) ) )
144 139 143 3 vtocl 
 |-  ( ( ph /\ ( ( 1st ` s ) oF + ( ( ( ( 2nd ` s ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` s ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K ) ) -> C e. ( 0 ... N ) )
145 138 144 sylan2 
 |-  ( ( ph /\ ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ j e. ( 0 ... N ) ) ) -> C e. ( 0 ... N ) )
146 145 an12s 
 |-  ( ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( ph /\ j e. ( 0 ... N ) ) ) -> C e. ( 0 ... N ) )
147 146 ex 
 |-  ( s e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( ( ph /\ j e. ( 0 ... N ) ) -> C e. ( 0 ... N ) ) )
148 64 68 71 147 vtoclgaf 
 |-  ( <. T , U >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... N ) ) )
149 63 148 mpcom 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... N ) )
150 44 48 149 chvarfv 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) )
151 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
152 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
153 151 152 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
154 fzm1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ t / j ]_ [_ <. T , U >. / s ]_ C = N ) ) )
155 153 154 syl 
 |-  ( ph -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ t / j ]_ [_ <. T , U >. / s ]_ C = N ) ) )
156 155 adantr 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ t / j ]_ [_ <. T , U >. / s ]_ C = N ) ) )
157 150 156 mpbid 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ t / j ]_ [_ <. T , U >. / s ]_ C = N ) )
158 157 ord 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( -. [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C = N ) )
159 41 158 mt3d 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) )
160 159 adantrr 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) )
161 fzfi 
 |-  ( 0 ... ( N - 1 ) ) e. Fin
162 1 nncnd 
 |-  ( ph -> N e. CC )
163 1cnd 
 |-  ( ph -> 1 e. CC )
164 162 163 163 addsubd 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = ( ( N - 1 ) + 1 ) )
165 hashfz0 
 |-  ( N e. NN0 -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
166 151 165 syl 
 |-  ( ph -> ( # ` ( 0 ... N ) ) = ( N + 1 ) )
167 166 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ... N ) ) - 1 ) = ( ( N + 1 ) - 1 ) )
168 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
169 hashfz0 
 |-  ( ( N - 1 ) e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( N - 1 ) + 1 ) )
170 1 168 169 3syl 
 |-  ( ph -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( N - 1 ) + 1 ) )
171 164 167 170 3eqtr4rd 
 |-  ( ph -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( ( # ` ( 0 ... N ) ) - 1 ) )
172 hashdifsn 
 |-  ( ( ( 0 ... N ) e. Fin /\ t e. ( 0 ... N ) ) -> ( # ` ( ( 0 ... N ) \ { t } ) ) = ( ( # ` ( 0 ... N ) ) - 1 ) )
173 14 172 mpan 
 |-  ( t e. ( 0 ... N ) -> ( # ` ( ( 0 ... N ) \ { t } ) ) = ( ( # ` ( 0 ... N ) ) - 1 ) )
174 173 eqcomd 
 |-  ( t e. ( 0 ... N ) -> ( ( # ` ( 0 ... N ) ) - 1 ) = ( # ` ( ( 0 ... N ) \ { t } ) ) )
175 171 174 sylan9eq 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( ( 0 ... N ) \ { t } ) ) )
176 diffi 
 |-  ( ( 0 ... N ) e. Fin -> ( ( 0 ... N ) \ { t } ) e. Fin )
177 14 176 ax-mp 
 |-  ( ( 0 ... N ) \ { t } ) e. Fin
178 hashen 
 |-  ( ( ( 0 ... ( N - 1 ) ) e. Fin /\ ( ( 0 ... N ) \ { t } ) e. Fin ) -> ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( ( 0 ... N ) \ { t } ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { t } ) ) )
179 161 177 178 mp2an 
 |-  ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( ( 0 ... N ) \ { t } ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { t } ) )
180 175 179 sylib 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { t } ) )
181 phpreu 
 |-  ( ( ( 0 ... ( N - 1 ) ) e. Fin /\ ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { t } ) ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
182 161 180 181 sylancr 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
183 182 biimpd 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C -> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
184 183 impr 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C )
185 nfv 
 |-  F/ z i = [_ <. T , U >. / s ]_ C
186 nfcsb1v 
 |-  F/_ j [_ z / j ]_ [_ <. T , U >. / s ]_ C
187 186 nfeq2 
 |-  F/ j i = [_ z / j ]_ [_ <. T , U >. / s ]_ C
188 csbeq1a 
 |-  ( j = z -> [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
189 188 eqeq2d 
 |-  ( j = z -> ( i = [_ <. T , U >. / s ]_ C <-> i = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
190 185 187 189 cbvreuw 
 |-  ( E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C <-> E! z e. ( ( 0 ... N ) \ { t } ) i = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
191 eqeq1 
 |-  ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C -> ( i = [_ z / j ]_ [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
192 191 reubidv 
 |-  ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C -> ( E! z e. ( ( 0 ... N ) \ { t } ) i = [_ z / j ]_ [_ <. T , U >. / s ]_ C <-> E! z e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
193 190 192 syl5bb 
 |-  ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C -> ( E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C <-> E! z e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
194 193 rspcv 
 |-  ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C -> E! z e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
195 160 184 194 sylc 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> E! z e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
196 an32 
 |-  ( ( ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) /\ z e. ( ( 0 ... N ) \ { t } ) ) <-> ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
197 196 biimpi 
 |-  ( ( ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
198 197 adantll 
 |-  ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
199 eqeq2 
 |-  ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C -> ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C <-> i = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
200 rexsns 
 |-  ( E. j e. { t } i = [_ <. T , U >. / s ]_ C <-> [. t / j ]. i = [_ <. T , U >. / s ]_ C )
201 34 nfeq2 
 |-  F/ j i = [_ t / j ]_ [_ <. T , U >. / s ]_ C
202 36 eqeq2d 
 |-  ( j = t -> ( i = [_ <. T , U >. / s ]_ C <-> i = [_ t / j ]_ [_ <. T , U >. / s ]_ C ) )
203 201 202 sbciegf 
 |-  ( t e. _V -> ( [. t / j ]. i = [_ <. T , U >. / s ]_ C <-> i = [_ t / j ]_ [_ <. T , U >. / s ]_ C ) )
204 13 203 ax-mp 
 |-  ( [. t / j ]. i = [_ <. T , U >. / s ]_ C <-> i = [_ t / j ]_ [_ <. T , U >. / s ]_ C )
205 200 204 bitri 
 |-  ( E. j e. { t } i = [_ <. T , U >. / s ]_ C <-> i = [_ t / j ]_ [_ <. T , U >. / s ]_ C )
206 rexsns 
 |-  ( E. j e. { z } i = [_ <. T , U >. / s ]_ C <-> [. z / j ]. i = [_ <. T , U >. / s ]_ C )
207 vex 
 |-  z e. _V
208 187 189 sbciegf 
 |-  ( z e. _V -> ( [. z / j ]. i = [_ <. T , U >. / s ]_ C <-> i = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
209 207 208 ax-mp 
 |-  ( [. z / j ]. i = [_ <. T , U >. / s ]_ C <-> i = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
210 206 209 bitri 
 |-  ( E. j e. { z } i = [_ <. T , U >. / s ]_ C <-> i = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
211 199 205 210 3bitr4g 
 |-  ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C -> ( E. j e. { t } i = [_ <. T , U >. / s ]_ C <-> E. j e. { z } i = [_ <. T , U >. / s ]_ C ) )
212 211 orbi1d 
 |-  ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C -> ( ( E. j e. { t } i = [_ <. T , U >. / s ]_ C \/ E. j e. ( ( ( 0 ... N ) \ { t } ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) <-> ( E. j e. { z } i = [_ <. T , U >. / s ]_ C \/ E. j e. ( ( ( 0 ... N ) \ { t } ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) ) )
213 rexun 
 |-  ( E. j e. ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> ( E. j e. { t } i = [_ <. T , U >. / s ]_ C \/ E. j e. ( ( ( 0 ... N ) \ { t } ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
214 rexun 
 |-  ( E. j e. ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> ( E. j e. { z } i = [_ <. T , U >. / s ]_ C \/ E. j e. ( ( ( 0 ... N ) \ { t } ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
215 212 213 214 3bitr4g 
 |-  ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C -> ( E. j e. ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C ) )
216 215 adantl 
 |-  ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> ( E. j e. ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C ) )
217 eldifsni 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) -> z =/= t )
218 217 necomd 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) -> t =/= z )
219 dif32 
 |-  ( ( ( 0 ... N ) \ { t } ) \ { z } ) = ( ( ( 0 ... N ) \ { z } ) \ { t } )
220 219 uneq2i 
 |-  ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) = ( { t } u. ( ( ( 0 ... N ) \ { z } ) \ { t } ) )
221 snssi 
 |-  ( t e. ( ( 0 ... N ) \ { z } ) -> { t } C_ ( ( 0 ... N ) \ { z } ) )
222 eldifsn 
 |-  ( t e. ( ( 0 ... N ) \ { z } ) <-> ( t e. ( 0 ... N ) /\ t =/= z ) )
223 undif 
 |-  ( { t } C_ ( ( 0 ... N ) \ { z } ) <-> ( { t } u. ( ( ( 0 ... N ) \ { z } ) \ { t } ) ) = ( ( 0 ... N ) \ { z } ) )
224 221 222 223 3imtr3i 
 |-  ( ( t e. ( 0 ... N ) /\ t =/= z ) -> ( { t } u. ( ( ( 0 ... N ) \ { z } ) \ { t } ) ) = ( ( 0 ... N ) \ { z } ) )
225 220 224 syl5eq 
 |-  ( ( t e. ( 0 ... N ) /\ t =/= z ) -> ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) = ( ( 0 ... N ) \ { z } ) )
226 218 225 sylan2 
 |-  ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) = ( ( 0 ... N ) \ { z } ) )
227 226 rexeqdv 
 |-  ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( E. j e. ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
228 227 adantr 
 |-  ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> ( E. j e. ( { t } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
229 snssi 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) -> { z } C_ ( ( 0 ... N ) \ { t } ) )
230 undif 
 |-  ( { z } C_ ( ( 0 ... N ) \ { t } ) <-> ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) = ( ( 0 ... N ) \ { t } ) )
231 229 230 sylib 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) -> ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) = ( ( 0 ... N ) \ { t } ) )
232 231 rexeqdv 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) -> ( E. j e. ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
233 232 ad2antlr 
 |-  ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> ( E. j e. ( { z } u. ( ( ( 0 ... N ) \ { t } ) \ { z } ) ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
234 216 228 233 3bitr3d 
 |-  ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> ( E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
235 234 ralbidv 
 |-  ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) )
236 235 biimpar 
 |-  ( ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C )
237 236 an32s 
 |-  ( ( ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C )
238 198 237 sylan 
 |-  ( ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C )
239 simpl 
 |-  ( ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) -> t e. ( 0 ... N ) )
240 239 anim2i 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> ( ph /\ t e. ( 0 ... N ) ) )
241 necom 
 |-  ( z =/= t <-> t =/= z )
242 241 biimpi 
 |-  ( z =/= t -> t =/= z )
243 242 adantl 
 |-  ( ( z e. ( 0 ... N ) /\ z =/= t ) -> t =/= z )
244 243 anim2i 
 |-  ( ( t e. ( 0 ... N ) /\ ( z e. ( 0 ... N ) /\ z =/= t ) ) -> ( t e. ( 0 ... N ) /\ t =/= z ) )
245 eldifsn 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) <-> ( z e. ( 0 ... N ) /\ z =/= t ) )
246 245 anbi2i 
 |-  ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) <-> ( t e. ( 0 ... N ) /\ ( z e. ( 0 ... N ) /\ z =/= t ) ) )
247 244 246 222 3imtr4i 
 |-  ( ( t e. ( 0 ... N ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> t e. ( ( 0 ... N ) \ { z } ) )
248 247 adantll 
 |-  ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> t e. ( ( 0 ... N ) \ { z } ) )
249 248 adantr 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> t e. ( ( 0 ... N ) \ { z } ) )
250 34 nfel1 
 |-  F/ j [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) )
251 42 250 nfim 
 |-  F/ j ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) )
252 36 eleq1d 
 |-  ( j = t -> ( [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) ) )
253 46 252 imbi12d 
 |-  ( j = t -> ( ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) ) <-> ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) ) ) )
254 6 necomd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C =/= N )
255 254 neneqd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> -. [_ <. T , U >. / s ]_ C = N )
256 fzm1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> ( [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ <. T , U >. / s ]_ C = N ) ) )
257 153 256 syl 
 |-  ( ph -> ( [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> ( [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ <. T , U >. / s ]_ C = N ) ) )
258 257 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( [_ <. T , U >. / s ]_ C e. ( 0 ... N ) <-> ( [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ <. T , U >. / s ]_ C = N ) ) )
259 149 258 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) \/ [_ <. T , U >. / s ]_ C = N ) )
260 259 ord 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( -. [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) -> [_ <. T , U >. / s ]_ C = N ) )
261 255 260 mt3d 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) )
262 251 253 261 chvarfv 
 |-  ( ( ph /\ t e. ( 0 ... N ) ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) )
263 262 ad2antrr 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) )
264 eldifi 
 |-  ( z e. ( ( 0 ... N ) \ { t } ) -> z e. ( 0 ... N ) )
265 eleq1w 
 |-  ( t = z -> ( t e. ( 0 ... N ) <-> z e. ( 0 ... N ) ) )
266 265 anbi2d 
 |-  ( t = z -> ( ( ph /\ t e. ( 0 ... N ) ) <-> ( ph /\ z e. ( 0 ... N ) ) ) )
267 sneq 
 |-  ( t = z -> { t } = { z } )
268 267 difeq2d 
 |-  ( t = z -> ( ( 0 ... N ) \ { t } ) = ( ( 0 ... N ) \ { z } ) )
269 268 breq2d 
 |-  ( t = z -> ( ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { t } ) <-> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) ) )
270 266 269 imbi12d 
 |-  ( t = z -> ( ( ( ph /\ t e. ( 0 ... N ) ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { t } ) ) <-> ( ( ph /\ z e. ( 0 ... N ) ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) ) ) )
271 270 180 chvarvv 
 |-  ( ( ph /\ z e. ( 0 ... N ) ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) )
272 264 271 sylan2 
 |-  ( ( ph /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) )
273 272 adantlr 
 |-  ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) )
274 phpreu 
 |-  ( ( ( 0 ... ( N - 1 ) ) e. Fin /\ ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
275 161 274 mpan 
 |-  ( ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
276 275 biimpa 
 |-  ( ( ( 0 ... ( N - 1 ) ) ~~ ( ( 0 ... N ) \ { z } ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C )
277 273 276 sylan 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C )
278 eqeq1 
 |-  ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C -> ( i = [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
279 278 adantr 
 |-  ( ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C /\ j e. ( ( 0 ... N ) \ { z } ) ) -> ( i = [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
280 201 279 reubida 
 |-  ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C -> ( E! j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> E! j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
281 280 rspcv 
 |-  ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) -> ( A. i e. ( 0 ... ( N - 1 ) ) E! j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C -> E! j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
282 263 277 281 sylc 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> E! j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
283 reurmo 
 |-  ( E! j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> E* j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
284 282 283 syl 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> E* j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
285 nfv 
 |-  F/ i [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C
286 285 rmo3 
 |-  ( E* j e. ( ( 0 ... N ) \ { z } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> A. j e. ( ( 0 ... N ) \ { z } ) A. i e. ( ( 0 ... N ) \ { z } ) ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> j = i ) )
287 284 286 sylib 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. j e. ( ( 0 ... N ) \ { z } ) A. i e. ( ( 0 ... N ) \ { z } ) ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> j = i ) )
288 equcomi 
 |-  ( i = t -> t = i )
289 288 csbeq1d 
 |-  ( i = t -> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C )
290 sbsbc 
 |-  ( [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> [. i / j ]. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
291 vex 
 |-  i e. _V
292 sbceqg 
 |-  ( i e. _V -> ( [. i / j ]. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> [_ i / j ]_ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C ) )
293 34 csbconstgf 
 |-  ( i e. _V -> [_ i / j ]_ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ t / j ]_ [_ <. T , U >. / s ]_ C )
294 293 eqeq1d 
 |-  ( i e. _V -> ( [_ i / j ]_ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C ) )
295 292 294 bitrd 
 |-  ( i e. _V -> ( [. i / j ]. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C ) )
296 291 295 ax-mp 
 |-  ( [. i / j ]. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C )
297 290 296 bitri 
 |-  ( [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ i / j ]_ [_ <. T , U >. / s ]_ C )
298 289 297 sylibr 
 |-  ( i = t -> [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
299 298 biantrud 
 |-  ( i = t -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
300 299 bicomd 
 |-  ( i = t -> ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
301 eqeq2 
 |-  ( i = t -> ( j = i <-> j = t ) )
302 300 301 imbi12d 
 |-  ( i = t -> ( ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> j = i ) <-> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) ) )
303 302 rspcv 
 |-  ( t e. ( ( 0 ... N ) \ { z } ) -> ( A. i e. ( ( 0 ... N ) \ { z } ) ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> j = i ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) ) )
304 303 ralimdv 
 |-  ( t e. ( ( 0 ... N ) \ { z } ) -> ( A. j e. ( ( 0 ... N ) \ { z } ) A. i e. ( ( 0 ... N ) \ { z } ) ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C /\ [ i / j ] [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> j = i ) -> A. j e. ( ( 0 ... N ) \ { z } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) ) )
305 249 287 304 sylc 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. j e. ( ( 0 ... N ) \ { z } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) )
306 dif32 
 |-  ( ( ( 0 ... N ) \ { z } ) \ { t } ) = ( ( ( 0 ... N ) \ { t } ) \ { z } )
307 306 eleq2i 
 |-  ( j e. ( ( ( 0 ... N ) \ { z } ) \ { t } ) <-> j e. ( ( ( 0 ... N ) \ { t } ) \ { z } ) )
308 eldifsn 
 |-  ( j e. ( ( ( 0 ... N ) \ { z } ) \ { t } ) <-> ( j e. ( ( 0 ... N ) \ { z } ) /\ j =/= t ) )
309 eldifsn 
 |-  ( j e. ( ( ( 0 ... N ) \ { t } ) \ { z } ) <-> ( j e. ( ( 0 ... N ) \ { t } ) /\ j =/= z ) )
310 307 308 309 3bitr3ri 
 |-  ( ( j e. ( ( 0 ... N ) \ { t } ) /\ j =/= z ) <-> ( j e. ( ( 0 ... N ) \ { z } ) /\ j =/= t ) )
311 310 imbi1i 
 |-  ( ( ( j e. ( ( 0 ... N ) \ { t } ) /\ j =/= z ) -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> ( ( j e. ( ( 0 ... N ) \ { z } ) /\ j =/= t ) -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
312 impexp 
 |-  ( ( ( j e. ( ( 0 ... N ) \ { t } ) /\ j =/= z ) -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> ( j e. ( ( 0 ... N ) \ { t } ) -> ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
313 impexp 
 |-  ( ( ( j e. ( ( 0 ... N ) \ { z } ) /\ j =/= t ) -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> ( j e. ( ( 0 ... N ) \ { z } ) -> ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
314 311 312 313 3bitr3ri 
 |-  ( ( j e. ( ( 0 ... N ) \ { z } ) -> ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) <-> ( j e. ( ( 0 ... N ) \ { t } ) -> ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
315 314 albii 
 |-  ( A. j ( j e. ( ( 0 ... N ) \ { z } ) -> ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) <-> A. j ( j e. ( ( 0 ... N ) \ { t } ) -> ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
316 con34b 
 |-  ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) <-> ( -. j = t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
317 df-ne 
 |-  ( j =/= t <-> -. j = t )
318 317 imbi1i 
 |-  ( ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> ( -. j = t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
319 316 318 bitr4i 
 |-  ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) <-> ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
320 319 ralbii 
 |-  ( A. j e. ( ( 0 ... N ) \ { z } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) <-> A. j e. ( ( 0 ... N ) \ { z } ) ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
321 df-ral 
 |-  ( A. j e. ( ( 0 ... N ) \ { z } ) ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> A. j ( j e. ( ( 0 ... N ) \ { z } ) -> ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
322 320 321 bitri 
 |-  ( A. j e. ( ( 0 ... N ) \ { z } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) <-> A. j ( j e. ( ( 0 ... N ) \ { z } ) -> ( j =/= t -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
323 df-ral 
 |-  ( A. j e. ( ( 0 ... N ) \ { t } ) ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> A. j ( j e. ( ( 0 ... N ) \ { t } ) -> ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
324 315 322 323 3bitr4i 
 |-  ( A. j e. ( ( 0 ... N ) \ { z } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = t ) <-> A. j e. ( ( 0 ... N ) \ { t } ) ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
325 305 324 sylib 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. j e. ( ( 0 ... N ) \ { t } ) ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
326 df-ne 
 |-  ( j =/= z <-> -. j = z )
327 326 imbi1i 
 |-  ( ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> ( -. j = z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
328 con34b 
 |-  ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = z ) <-> ( -. j = z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
329 327 328 bitr4i 
 |-  ( ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = z ) )
330 ancr 
 |-  ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> j = z ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
331 329 330 sylbi 
 |-  ( ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
332 331 ralimi 
 |-  ( A. j e. ( ( 0 ... N ) \ { t } ) ( j =/= z -> -. [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> A. j e. ( ( 0 ... N ) \ { t } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
333 325 332 syl 
 |-  ( ( ( ( ph /\ t e. ( 0 ... N ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. j e. ( ( 0 ... N ) \ { t } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
334 240 333 sylanl1 
 |-  ( ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> A. j e. ( ( 0 ... N ) \ { t } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
335 201 278 rexbid 
 |-  ( i = [_ t / j ]_ [_ <. T , U >. / s ]_ C -> ( E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
336 335 rspcva 
 |-  ( ( [_ t / j ]_ [_ <. T , U >. / s ]_ C e. ( 0 ... ( N - 1 ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) -> E. j e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
337 262 336 sylan 
 |-  ( ( ( ph /\ t e. ( 0 ... N ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) -> E. j e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
338 337 anasss 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> E. j e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
339 338 ad2antrr 
 |-  ( ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> E. j e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C )
340 rexim 
 |-  ( A. j e. ( ( 0 ... N ) \ { t } ) ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) -> ( E. j e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C -> E. j e. ( ( 0 ... N ) \ { t } ) ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) ) )
341 334 339 340 sylc 
 |-  ( ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> E. j e. ( ( 0 ... N ) \ { t } ) ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
342 rexex 
 |-  ( E. j e. ( ( 0 ... N ) \ { t } ) ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) -> E. j ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
343 341 342 syl 
 |-  ( ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> E. j ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) )
344 34 186 nfeq 
 |-  F/ j [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C
345 188 eqeq2d 
 |-  ( j = z -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C ) )
346 344 345 equsexv 
 |-  ( E. j ( j = z /\ [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ <. T , U >. / s ]_ C ) <-> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
347 343 346 sylib 
 |-  ( ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) -> [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C )
348 238 347 impbida 
 |-  ( ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) /\ z e. ( ( 0 ... N ) \ { t } ) ) -> ( [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
349 348 reubidva 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> ( E! z e. ( ( 0 ... N ) \ { t } ) [_ t / j ]_ [_ <. T , U >. / s ]_ C = [_ z / j ]_ [_ <. T , U >. / s ]_ C <-> E! z e. ( ( 0 ... N ) \ { t } ) A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
350 195 349 mpbid 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> E! z e. ( ( 0 ... N ) \ { t } ) A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C )
351 an32 
 |-  ( ( ( z e. ( 0 ... N ) /\ z =/= t ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) <-> ( ( z e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) /\ z =/= t ) )
352 245 anbi1i 
 |-  ( ( z e. ( ( 0 ... N ) \ { t } ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) <-> ( ( z e. ( 0 ... N ) /\ z =/= t ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
353 sneq 
 |-  ( y = z -> { y } = { z } )
354 353 difeq2d 
 |-  ( y = z -> ( ( 0 ... N ) \ { y } ) = ( ( 0 ... N ) \ { z } ) )
355 354 rexeqdv 
 |-  ( y = z -> ( E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C <-> E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
356 355 ralbidv 
 |-  ( y = z -> ( A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C <-> A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
357 356 elrab 
 |-  ( z e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } <-> ( z e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
358 357 anbi1i 
 |-  ( ( z e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } /\ z =/= t ) <-> ( ( z e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) /\ z =/= t ) )
359 351 352 358 3bitr4i 
 |-  ( ( z e. ( ( 0 ... N ) \ { t } ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) <-> ( z e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } /\ z =/= t ) )
360 eldifsn 
 |-  ( z e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) <-> ( z e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } /\ z =/= t ) )
361 359 360 bitr4i 
 |-  ( ( z e. ( ( 0 ... N ) \ { t } ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) <-> z e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) )
362 361 eubii 
 |-  ( E! z ( z e. ( ( 0 ... N ) \ { t } ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) <-> E! z z e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) )
363 df-reu 
 |-  ( E! z e. ( ( 0 ... N ) \ { t } ) A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> E! z ( z e. ( ( 0 ... N ) \ { t } ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C ) )
364 euhash1 
 |-  ( ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) e. Fin -> ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) = 1 <-> E! z z e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) )
365 18 364 ax-mp 
 |-  ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) = 1 <-> E! z z e. ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) )
366 362 363 365 3bitr4i 
 |-  ( E! z e. ( ( 0 ... N ) \ { t } ) A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { z } ) i = [_ <. T , U >. / s ]_ C <-> ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) = 1 )
367 350 366 sylib 
 |-  ( ( ph /\ ( t e. ( 0 ... N ) /\ A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { t } ) i = [_ <. T , U >. / s ]_ C ) ) -> ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) = 1 )
368 31 367 sylan2b 
 |-  ( ( ph /\ t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) -> ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) = 1 )
369 368 oveq1d 
 |-  ( ( ph /\ t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) -> ( ( # ` ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } \ { t } ) ) + 1 ) = ( 1 + 1 ) )
370 26 369 eqtr3d 
 |-  ( ( ph /\ t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) -> ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) = ( 1 + 1 ) )
371 12 370 breqtrrid 
 |-  ( ( ph /\ t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )
372 371 ex 
 |-  ( ph -> ( t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) ) )
373 372 exlimdv 
 |-  ( ph -> ( E. t t e. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) ) )
374 7 373 syl5bi 
 |-  ( ph -> ( -. { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } = (/) -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) ) )
375 dvds0 
 |-  ( 2 e. ZZ -> 2 || 0 )
376 8 375 ax-mp 
 |-  2 || 0
377 hash0 
 |-  ( # ` (/) ) = 0
378 376 377 breqtrri 
 |-  2 || ( # ` (/) )
379 fveq2 
 |-  ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } = (/) -> ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) = ( # ` (/) ) )
380 378 379 breqtrrid 
 |-  ( { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } = (/) -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )
381 374 380 pm2.61d2 
 |-  ( ph -> 2 || ( # ` { y e. ( 0 ... N ) | A. i e. ( 0 ... ( N - 1 ) ) E. j e. ( ( 0 ... N ) \ { y } ) i = [_ <. T , U >. / s ]_ C } ) )