Metamath Proof Explorer

Theorem eldioph2lem2

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

Ref Expression
Assertion eldioph2lem2 
|- ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> E. c ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )

Proof

Step Hyp Ref Expression
1 simplr 
 |-  ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> -. S e. Fin )
2 fzfi 
 |-  ( 1 ... N ) e. Fin
3 difinf 
 |-  ( ( -. S e. Fin /\ ( 1 ... N ) e. Fin ) -> -. ( S \ ( 1 ... N ) ) e. Fin )
4 1 2 3 sylancl 
 |-  ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> -. ( S \ ( 1 ... N ) ) e. Fin )
5 fzfi 
 |-  ( 1 ... A ) e. Fin
6 diffi 
 |-  ( ( 1 ... A ) e. Fin -> ( ( 1 ... A ) \ ( 1 ... N ) ) e. Fin )
7 5 6 ax-mp 
 |-  ( ( 1 ... A ) \ ( 1 ... N ) ) e. Fin
8 isinffi 
 |-  ( ( -. ( S \ ( 1 ... N ) ) e. Fin /\ ( ( 1 ... A ) \ ( 1 ... N ) ) e. Fin ) -> E. a a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) )
9 4 7 8 sylancl 
 |-  ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> E. a a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) )
10 f1f1orn 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-onto-> ran a )
11 10 adantl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-onto-> ran a )
12 f1oi 
 |-  ( _I |` ( 1 ... N ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )
13 12 a1i 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( _I |` ( 1 ... N ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
14 disjdifr 
 |-  ( ( ( 1 ... A ) \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/)
15 14 a1i 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( ( 1 ... A ) \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/) )
16 f1f 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> a : ( ( 1 ... A ) \ ( 1 ... N ) ) --> ( S \ ( 1 ... N ) ) )
17 16 frnd 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> ran a C_ ( S \ ( 1 ... N ) ) )
18 17 adantl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ran a C_ ( S \ ( 1 ... N ) ) )
19 18 ssrind 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ran a i^i ( 1 ... N ) ) C_ ( ( S \ ( 1 ... N ) ) i^i ( 1 ... N ) ) )
20 disjdifr 
 |-  ( ( S \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/)
21 19 20 sseqtrdi 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ran a i^i ( 1 ... N ) ) C_ (/) )
22 ss0 
 |-  ( ( ran a i^i ( 1 ... N ) ) C_ (/) -> ( ran a i^i ( 1 ... N ) ) = (/) )
23 21 22 syl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ran a i^i ( 1 ... N ) ) = (/) )
24 f1oun 
 |-  ( ( ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-onto-> ran a /\ ( _I |` ( 1 ... N ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) /\ ( ( ( ( 1 ... A ) \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/) /\ ( ran a i^i ( 1 ... N ) ) = (/) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ran a u. ( 1 ... N ) ) )
25 11 13 15 23 24 syl22anc 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ran a u. ( 1 ... N ) ) )
26 f1of1 
 |-  ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-onto-> ( ran a u. ( 1 ... N ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-> ( ran a u. ( 1 ... N ) ) )
27 25 26 syl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-> ( ran a u. ( 1 ... N ) ) )
28 uncom 
 |-  ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) = ( ( 1 ... N ) u. ( ( 1 ... A ) \ ( 1 ... N ) ) )
29 simplrr 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> A e. ( ZZ>= ` N ) )
30 fzss2 
 |-  ( A e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... A ) )
31 29 30 syl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( 1 ... N ) C_ ( 1 ... A ) )
32 undif 
 |-  ( ( 1 ... N ) C_ ( 1 ... A ) <-> ( ( 1 ... N ) u. ( ( 1 ... A ) \ ( 1 ... N ) ) ) = ( 1 ... A ) )
33 31 32 sylib 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( 1 ... N ) u. ( ( 1 ... A ) \ ( 1 ... N ) ) ) = ( 1 ... A ) )
34 28 33 syl5eq 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) = ( 1 ... A ) )
35 f1eq2 
 |-  ( ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) = ( 1 ... A ) -> ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-> ( ran a u. ( 1 ... N ) ) <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> ( ran a u. ( 1 ... N ) ) ) )
36 34 35 syl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-> ( ran a u. ( 1 ... N ) ) <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> ( ran a u. ( 1 ... N ) ) ) )
37 27 36 mpbid 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> ( ran a u. ( 1 ... N ) ) )
38 17 difss2d 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> ran a C_ S )
39 38 adantl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ran a C_ S )
40 simplrl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( 1 ... N ) C_ S )
41 39 40 unssd 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ran a u. ( 1 ... N ) ) C_ S )
42 f1ss 
 |-  ( ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> ( ran a u. ( 1 ... N ) ) /\ ( ran a u. ( 1 ... N ) ) C_ S ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> S )
43 37 41 42 syl2anc 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> S )
44 resundir 
 |-  ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) )
45 dmres 
 |-  dom ( a |` ( 1 ... N ) ) = ( ( 1 ... N ) i^i dom a )
46 incom 
 |-  ( ( 1 ... N ) i^i dom a ) = ( dom a i^i ( 1 ... N ) )
47 f1dm 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> dom a = ( ( 1 ... A ) \ ( 1 ... N ) ) )
48 47 adantl 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> dom a = ( ( 1 ... A ) \ ( 1 ... N ) ) )
49 48 ineq1d 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( dom a i^i ( 1 ... N ) ) = ( ( ( 1 ... A ) \ ( 1 ... N ) ) i^i ( 1 ... N ) ) )
50 49 14 eqtrdi 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( dom a i^i ( 1 ... N ) ) = (/) )
51 46 50 syl5eq 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( 1 ... N ) i^i dom a ) = (/) )
52 45 51 syl5eq 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> dom ( a |` ( 1 ... N ) ) = (/) )
53 relres 
 |-  Rel ( a |` ( 1 ... N ) )
54 reldm0 
 |-  ( Rel ( a |` ( 1 ... N ) ) -> ( ( a |` ( 1 ... N ) ) = (/) <-> dom ( a |` ( 1 ... N ) ) = (/) ) )
55 53 54 ax-mp 
 |-  ( ( a |` ( 1 ... N ) ) = (/) <-> dom ( a |` ( 1 ... N ) ) = (/) )
56 52 55 sylibr 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( a |` ( 1 ... N ) ) = (/) )
57 residm 
 |-  ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) )
58 57 a1i 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) )
59 56 58 uneq12d 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) ) = ( (/) u. ( _I |` ( 1 ... N ) ) ) )
60 uncom 
 |-  ( (/) u. ( _I |` ( 1 ... N ) ) ) = ( ( _I |` ( 1 ... N ) ) u. (/) )
61 un0 
 |-  ( ( _I |` ( 1 ... N ) ) u. (/) ) = ( _I |` ( 1 ... N ) )
62 60 61 eqtri 
 |-  ( (/) u. ( _I |` ( 1 ... N ) ) ) = ( _I |` ( 1 ... N ) )
63 59 62 eqtrdi 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) ) = ( _I |` ( 1 ... N ) ) )
64 44 63 syl5eq 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) )
65 vex 
 |-  a e. _V
66 ovex 
 |-  ( 1 ... N ) e. _V
67 resiexg 
 |-  ( ( 1 ... N ) e. _V -> ( _I |` ( 1 ... N ) ) e. _V )
68 66 67 ax-mp 
 |-  ( _I |` ( 1 ... N ) ) e. _V
69 65 68 unex 
 |-  ( a u. ( _I |` ( 1 ... N ) ) ) e. _V
70 f1eq1 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( c : ( 1 ... A ) -1-1-> S <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> S ) )
71 reseq1 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( c |` ( 1 ... N ) ) = ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) )
72 71 eqeq1d 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) <-> ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
73 70 72 anbi12d 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) <-> ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> S /\ ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) ) )
74 69 73 spcev 
 |-  ( ( ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> S /\ ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) -> E. c ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
75 43 64 74 syl2anc 
 |-  ( ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) /\ a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) ) -> E. c ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
76 9 75 exlimddv 
 |-  ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> E. c ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )