Metamath Proof Explorer

Theorem eldioph2lem1

Description: Lemma for eldioph2 . Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion eldioph2lem1 
|- ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> E. d e. ( ZZ>= ` N ) E. e e. _V ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 1 3ad2ant1 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> N e. RR )
3 2 recnd 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> N e. CC )
4 ax-1cn 
 |-  1 e. CC
5 addcom 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( N + 1 ) = ( 1 + N ) )
6 3 4 5 sylancl 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( N + 1 ) = ( 1 + N ) )
7 diffi 
 |-  ( A e. Fin -> ( A \ ( 1 ... N ) ) e. Fin )
8 7 3ad2ant2 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( A \ ( 1 ... N ) ) e. Fin )
9 fzfid 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( 1 ... N ) e. Fin )
10 disjdifr 
 |-  ( ( A \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/)
11 10 a1i 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( A \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/) )
12 hashun 
 |-  ( ( ( A \ ( 1 ... N ) ) e. Fin /\ ( 1 ... N ) e. Fin /\ ( ( A \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/) ) -> ( # ` ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) ) = ( ( # ` ( A \ ( 1 ... N ) ) ) + ( # ` ( 1 ... N ) ) ) )
13 8 9 11 12 syl3anc 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) ) = ( ( # ` ( A \ ( 1 ... N ) ) ) + ( # ` ( 1 ... N ) ) ) )
14 uncom 
 |-  ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) = ( ( 1 ... N ) u. ( A \ ( 1 ... N ) ) )
15 simp3 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( 1 ... N ) C_ A )
16 undif 
 |-  ( ( 1 ... N ) C_ A <-> ( ( 1 ... N ) u. ( A \ ( 1 ... N ) ) ) = A )
17 15 16 sylib 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( 1 ... N ) u. ( A \ ( 1 ... N ) ) ) = A )
18 14 17 syl5eq 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) = A )
19 18 fveq2d 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) ) = ( # ` A ) )
20 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
21 20 3ad2ant1 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( 1 ... N ) ) = N )
22 21 oveq2d 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( # ` ( A \ ( 1 ... N ) ) ) + ( # ` ( 1 ... N ) ) ) = ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) )
23 13 19 22 3eqtr3d 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` A ) = ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) )
24 6 23 oveq12d 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( N + 1 ) ... ( # ` A ) ) = ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) )
25 24 fveq2d 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( ( N + 1 ) ... ( # ` A ) ) ) = ( # ` ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ) )
26 1zzd 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> 1 e. ZZ )
27 hashcl 
 |-  ( ( A \ ( 1 ... N ) ) e. Fin -> ( # ` ( A \ ( 1 ... N ) ) ) e. NN0 )
28 8 27 syl 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( A \ ( 1 ... N ) ) ) e. NN0 )
29 28 nn0zd 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( A \ ( 1 ... N ) ) ) e. ZZ )
30 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
31 30 3ad2ant1 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> N e. ZZ )
32 fzen 
 |-  ( ( 1 e. ZZ /\ ( # ` ( A \ ( 1 ... N ) ) ) e. ZZ /\ N e. ZZ ) -> ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ~~ ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) )
33 26 29 31 32 syl3anc 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ~~ ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) )
34 33 ensymd 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ~~ ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) )
35 fzfi 
 |-  ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) e. Fin
36 fzfi 
 |-  ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) e. Fin
37 hashen 
 |-  ( ( ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) e. Fin /\ ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) e. Fin ) -> ( ( # ` ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ) = ( # ` ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ) <-> ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ~~ ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ) )
38 35 36 37 mp2an 
 |-  ( ( # ` ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ) = ( # ` ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ) <-> ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ~~ ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) )
39 34 38 sylibr 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( ( 1 + N ) ... ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) ) ) = ( # ` ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ) )
40 hashfz1 
 |-  ( ( # ` ( A \ ( 1 ... N ) ) ) e. NN0 -> ( # ` ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ) = ( # ` ( A \ ( 1 ... N ) ) ) )
41 28 40 syl 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( 1 ... ( # ` ( A \ ( 1 ... N ) ) ) ) ) = ( # ` ( A \ ( 1 ... N ) ) ) )
42 25 39 41 3eqtrd 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( # ` ( ( N + 1 ) ... ( # ` A ) ) ) = ( # ` ( A \ ( 1 ... N ) ) ) )
43 fzfi 
 |-  ( ( N + 1 ) ... ( # ` A ) ) e. Fin
44 hashen 
 |-  ( ( ( ( N + 1 ) ... ( # ` A ) ) e. Fin /\ ( A \ ( 1 ... N ) ) e. Fin ) -> ( ( # ` ( ( N + 1 ) ... ( # ` A ) ) ) = ( # ` ( A \ ( 1 ... N ) ) ) <-> ( ( N + 1 ) ... ( # ` A ) ) ~~ ( A \ ( 1 ... N ) ) ) )
45 43 8 44 sylancr 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( # ` ( ( N + 1 ) ... ( # ` A ) ) ) = ( # ` ( A \ ( 1 ... N ) ) ) <-> ( ( N + 1 ) ... ( # ` A ) ) ~~ ( A \ ( 1 ... N ) ) ) )
46 42 45 mpbid 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> ( ( N + 1 ) ... ( # ` A ) ) ~~ ( A \ ( 1 ... N ) ) )
47 bren 
 |-  ( ( ( N + 1 ) ... ( # ` A ) ) ~~ ( A \ ( 1 ... N ) ) <-> E. a a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) )
48 46 47 sylib 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> E. a a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) )
49 simpl1 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> N e. NN0 )
50 49 nn0zd 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> N e. ZZ )
51 simpl2 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> A e. Fin )
52 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
53 51 52 syl 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( # ` A ) e. NN0 )
54 53 nn0zd 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( # ` A ) e. ZZ )
55 nn0addge2 
 |-  ( ( N e. RR /\ ( # ` ( A \ ( 1 ... N ) ) ) e. NN0 ) -> N <_ ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) )
56 2 28 55 syl2anc 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> N <_ ( ( # ` ( A \ ( 1 ... N ) ) ) + N ) )
57 56 23 breqtrrd 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> N <_ ( # ` A ) )
58 57 adantr 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> N <_ ( # ` A ) )
59 eluz2 
 |-  ( ( # ` A ) e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ ( # ` A ) e. ZZ /\ N <_ ( # ` A ) ) )
60 50 54 58 59 syl3anbrc 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( # ` A ) e. ( ZZ>= ` N ) )
61 vex 
 |-  a e. _V
62 ovex 
 |-  ( 1 ... N ) e. _V
63 resiexg 
 |-  ( ( 1 ... N ) e. _V -> ( _I |` ( 1 ... N ) ) e. _V )
64 62 63 ax-mp 
 |-  ( _I |` ( 1 ... N ) ) e. _V
65 61 64 unex 
 |-  ( a u. ( _I |` ( 1 ... N ) ) ) e. _V
66 65 a1i 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) e. _V )
67 simpr 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) )
68 f1oi 
 |-  ( _I |` ( 1 ... N ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )
69 68 a1i 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( _I |` ( 1 ... N ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
70 incom 
 |-  ( ( ( N + 1 ) ... ( # ` A ) ) i^i ( 1 ... N ) ) = ( ( 1 ... N ) i^i ( ( N + 1 ) ... ( # ` A ) ) )
71 49 nn0red 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> N e. RR )
72 71 ltp1d 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> N < ( N + 1 ) )
73 fzdisj 
 |-  ( N < ( N + 1 ) -> ( ( 1 ... N ) i^i ( ( N + 1 ) ... ( # ` A ) ) ) = (/) )
74 72 73 syl 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( 1 ... N ) i^i ( ( N + 1 ) ... ( # ` A ) ) ) = (/) )
75 70 74 syl5eq 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( ( N + 1 ) ... ( # ` A ) ) i^i ( 1 ... N ) ) = (/) )
76 10 a1i 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( A \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/) )
77 f1oun 
 |-  ( ( ( a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) /\ ( _I |` ( 1 ... N ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) /\ ( ( ( ( N + 1 ) ... ( # ` A ) ) i^i ( 1 ... N ) ) = (/) /\ ( ( A \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) )
78 67 69 75 76 77 syl22anc 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) )
79 uncom 
 |-  ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) = ( ( 1 ... N ) u. ( ( N + 1 ) ... ( # ` A ) ) )
80 fzsplit1nn0 
 |-  ( ( N e. NN0 /\ ( # ` A ) e. NN0 /\ N <_ ( # ` A ) ) -> ( 1 ... ( # ` A ) ) = ( ( 1 ... N ) u. ( ( N + 1 ) ... ( # ` A ) ) ) )
81 49 53 58 80 syl3anc 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( 1 ... ( # ` A ) ) = ( ( 1 ... N ) u. ( ( N + 1 ) ... ( # ` A ) ) ) )
82 79 81 eqtr4id 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) = ( 1 ... ( # ` A ) ) )
83 simpl3 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( 1 ... N ) C_ A )
84 83 16 sylib 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( 1 ... N ) u. ( A \ ( 1 ... N ) ) ) = A )
85 14 84 syl5eq 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) = A )
86 f1oeq23 
 |-  ( ( ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) = ( 1 ... ( # ` A ) ) /\ ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) = A ) -> ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) )
87 82 85 86 syl2anc 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( N + 1 ) ... ( # ` A ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ( A \ ( 1 ... N ) ) u. ( 1 ... N ) ) <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) )
88 78 87 mpbid 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
89 resundir 
 |-  ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) )
90 dmres 
 |-  dom ( a |` ( 1 ... N ) ) = ( ( 1 ... N ) i^i dom a )
91 f1odm 
 |-  ( a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) -> dom a = ( ( N + 1 ) ... ( # ` A ) ) )
92 91 adantl 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> dom a = ( ( N + 1 ) ... ( # ` A ) ) )
93 92 ineq2d 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( 1 ... N ) i^i dom a ) = ( ( 1 ... N ) i^i ( ( N + 1 ) ... ( # ` A ) ) ) )
94 93 74 eqtrd 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( 1 ... N ) i^i dom a ) = (/) )
95 90 94 syl5eq 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> dom ( a |` ( 1 ... N ) ) = (/) )
96 relres 
 |-  Rel ( a |` ( 1 ... N ) )
97 reldm0 
 |-  ( Rel ( a |` ( 1 ... N ) ) -> ( ( a |` ( 1 ... N ) ) = (/) <-> dom ( a |` ( 1 ... N ) ) = (/) ) )
98 96 97 ax-mp 
 |-  ( ( a |` ( 1 ... N ) ) = (/) <-> dom ( a |` ( 1 ... N ) ) = (/) )
99 95 98 sylibr 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( a |` ( 1 ... N ) ) = (/) )
100 residm 
 |-  ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) )
101 100 a1i 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) )
102 99 101 uneq12d 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) ) = ( (/) u. ( _I |` ( 1 ... N ) ) ) )
103 uncom 
 |-  ( (/) u. ( _I |` ( 1 ... N ) ) ) = ( ( _I |` ( 1 ... N ) ) u. (/) )
104 un0 
 |-  ( ( _I |` ( 1 ... N ) ) u. (/) ) = ( _I |` ( 1 ... N ) )
105 103 104 eqtri 
 |-  ( (/) u. ( _I |` ( 1 ... N ) ) ) = ( _I |` ( 1 ... N ) )
106 102 105 eqtrdi 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) ) = ( _I |` ( 1 ... N ) ) )
107 89 106 syl5eq 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) )
108 oveq2 
 |-  ( d = ( # ` A ) -> ( 1 ... d ) = ( 1 ... ( # ` A ) ) )
109 108 f1oeq2d 
 |-  ( d = ( # ` A ) -> ( e : ( 1 ... d ) -1-1-onto-> A <-> e : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) )
110 109 anbi1d 
 |-  ( d = ( # ` A ) -> ( ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) <-> ( e : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) )
111 f1oeq1 
 |-  ( e = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( e : ( 1 ... ( # ` A ) ) -1-1-onto-> A <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) )
112 reseq1 
 |-  ( e = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( e |` ( 1 ... N ) ) = ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) )
113 112 eqeq1d 
 |-  ( e = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) <-> ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
114 111 113 anbi12d 
 |-  ( e = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( ( e : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) <-> ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) )
115 110 114 rspc2ev 
 |-  ( ( ( # ` A ) e. ( ZZ>= ` N ) /\ ( a u. ( _I |` ( 1 ... N ) ) ) e. _V /\ ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... ( # ` A ) ) -1-1-onto-> A /\ ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) -> E. d e. ( ZZ>= ` N ) E. e e. _V ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
116 60 66 88 107 115 syl112anc 
 |-  ( ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) /\ a : ( ( N + 1 ) ... ( # ` A ) ) -1-1-onto-> ( A \ ( 1 ... N ) ) ) -> E. d e. ( ZZ>= ` N ) E. e e. _V ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
117 48 116 exlimddv 
 |-  ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> E. d e. ( ZZ>= ` N ) E. e e. _V ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )