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