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 incom 
 |-  ( ( ( 1 ... A ) \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = ( ( 1 ... N ) i^i ( ( 1 ... A ) \ ( 1 ... N ) ) )
15 disjdif 
 |-  ( ( 1 ... N ) i^i ( ( 1 ... A ) \ ( 1 ... N ) ) ) = (/)
16 14 15 eqtri 
 |-  ( ( ( 1 ... A ) \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/)
17 16 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 ) ) = (/) )
18 f1f 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> a : ( ( 1 ... A ) \ ( 1 ... N ) ) --> ( S \ ( 1 ... N ) ) )
19 18 frnd 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> ran a C_ ( S \ ( 1 ... N ) ) )
20 19 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 ) ) )
21 20 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 ) ) )
22 incom 
 |-  ( ( S \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = ( ( 1 ... N ) i^i ( S \ ( 1 ... N ) ) )
23 disjdif 
 |-  ( ( 1 ... N ) i^i ( S \ ( 1 ... N ) ) ) = (/)
24 22 23 eqtri 
 |-  ( ( S \ ( 1 ... N ) ) i^i ( 1 ... N ) ) = (/)
25 21 24 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_ (/) )
26 ss0 
 |-  ( ( ran a i^i ( 1 ... N ) ) C_ (/) -> ( ran a i^i ( 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 ) ) ) -> ( ran a i^i ( 1 ... N ) ) = (/) )
28 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 ) ) )
29 11 13 17 27 28 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 ) ) )
30 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 ) ) )
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 ) ) ) -> ( a u. ( _I |` ( 1 ... N ) ) ) : ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) -1-1-> ( ran a u. ( 1 ... N ) ) )
32 uncom 
 |-  ( ( ( 1 ... A ) \ ( 1 ... N ) ) u. ( 1 ... N ) ) = ( ( 1 ... N ) u. ( ( 1 ... A ) \ ( 1 ... N ) ) )
33 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 ) )
34 fzss2 
 |-  ( A e. ( ZZ>= ` N ) -> ( 1 ... N ) C_ ( 1 ... A ) )
35 33 34 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 ) )
36 undif 
 |-  ( ( 1 ... N ) C_ ( 1 ... A ) <-> ( ( 1 ... N ) u. ( ( 1 ... A ) \ ( 1 ... N ) ) ) = ( 1 ... A ) )
37 35 36 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 ) )
38 32 37 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 ) )
39 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 ) ) ) )
40 38 39 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 ) ) ) )
41 31 40 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 ) ) )
42 19 difss2d 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> ran a C_ S )
43 42 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 )
44 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 )
45 43 44 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 )
46 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 )
47 41 45 46 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 )
48 resundir 
 |-  ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( ( a |` ( 1 ... N ) ) u. ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) )
49 dmres 
 |-  dom ( a |` ( 1 ... N ) ) = ( ( 1 ... N ) i^i dom a )
50 incom 
 |-  ( ( 1 ... N ) i^i dom a ) = ( dom a i^i ( 1 ... N ) )
51 f1dm 
 |-  ( a : ( ( 1 ... A ) \ ( 1 ... N ) ) -1-1-> ( S \ ( 1 ... N ) ) -> dom a = ( ( 1 ... A ) \ ( 1 ... N ) ) )
52 51 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 ) ) )
53 52 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 ) ) )
54 53 16 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 ) ) = (/) )
55 50 54 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 ) = (/) )
56 49 55 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 ) ) = (/) )
57 relres 
 |-  Rel ( a |` ( 1 ... N ) )
58 reldm0 
 |-  ( Rel ( a |` ( 1 ... N ) ) -> ( ( a |` ( 1 ... N ) ) = (/) <-> dom ( a |` ( 1 ... N ) ) = (/) ) )
59 57 58 ax-mp 
 |-  ( ( a |` ( 1 ... N ) ) = (/) <-> dom ( a |` ( 1 ... N ) ) = (/) )
60 56 59 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 ) ) = (/) )
61 residm 
 |-  ( ( _I |` ( 1 ... N ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) )
62 61 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 ) ) )
63 60 62 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 ) ) ) )
64 uncom 
 |-  ( (/) u. ( _I |` ( 1 ... N ) ) ) = ( ( _I |` ( 1 ... N ) ) u. (/) )
65 un0 
 |-  ( ( _I |` ( 1 ... N ) ) u. (/) ) = ( _I |` ( 1 ... N ) )
66 64 65 eqtri 
 |-  ( (/) u. ( _I |` ( 1 ... N ) ) ) = ( _I |` ( 1 ... N ) )
67 63 66 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 ) ) )
68 48 67 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 ) ) )
69 vex 
 |-  a e. _V
70 ovex 
 |-  ( 1 ... N ) e. _V
71 resiexg 
 |-  ( ( 1 ... N ) e. _V -> ( _I |` ( 1 ... N ) ) e. _V )
72 70 71 ax-mp 
 |-  ( _I |` ( 1 ... N ) ) e. _V
73 69 72 unex 
 |-  ( a u. ( _I |` ( 1 ... N ) ) ) e. _V
74 f1eq1 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( c : ( 1 ... A ) -1-1-> S <-> ( a u. ( _I |` ( 1 ... N ) ) ) : ( 1 ... A ) -1-1-> S ) )
75 reseq1 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( c |` ( 1 ... N ) ) = ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) )
76 75 eqeq1d 
 |-  ( c = ( a u. ( _I |` ( 1 ... N ) ) ) -> ( ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) <-> ( ( a u. ( _I |` ( 1 ... N ) ) ) |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
77 74 76 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 ) ) ) ) )
78 73 77 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 ) ) ) )
79 47 68 78 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 ) ) ) )
80 9 79 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 ) ) ) )