Metamath Proof Explorer

Theorem injresinj

Description: A function whose restriction is injective and the values of the remaining arguments are different from all other values is injective itself. (Contributed by Alexander van der Vekens, 31-Oct-2017)

Ref Expression
Assertion injresinj 
|- ( K e. NN0 -> ( ( F : ( 0 ... K ) --> V /\ Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F ` 0 ) =/= ( F ` K ) ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) ) )

Proof

Step Hyp Ref Expression
1 fzo0ss1 
 |-  ( 1 ..^ K ) C_ ( 0 ..^ K )
2 fzossfz 
 |-  ( 0 ..^ K ) C_ ( 0 ... K )
3 1 2 sstri 
 |-  ( 1 ..^ K ) C_ ( 0 ... K )
4 fssres 
 |-  ( ( F : ( 0 ... K ) --> V /\ ( 1 ..^ K ) C_ ( 0 ... K ) ) -> ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V )
5 3 4 mpan2 
 |-  ( F : ( 0 ... K ) --> V -> ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V )
6 5 biantrud 
 |-  ( F : ( 0 ... K ) --> V -> ( Fun `' ( F |` ( 1 ..^ K ) ) <-> ( Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V ) ) )
7 ancom 
 |-  ( ( Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V ) <-> ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V /\ Fun `' ( F |` ( 1 ..^ K ) ) ) )
8 df-f1 
 |-  ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V <-> ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V /\ Fun `' ( F |` ( 1 ..^ K ) ) ) )
9 7 8 bitr4i 
 |-  ( ( Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V ) <-> ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V )
10 6 9 bitrdi 
 |-  ( F : ( 0 ... K ) --> V -> ( Fun `' ( F |` ( 1 ..^ K ) ) <-> ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V ) )
11 simp-4r 
 |-  ( ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> F : ( 0 ... K ) --> V )
12 dff13 
 |-  ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V <-> ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) --> V /\ A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) ) )
13 fveqeq2 
 |-  ( v = x -> ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) <-> ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` w ) ) )
14 equequ1 
 |-  ( v = x -> ( v = w <-> x = w ) )
15 13 14 imbi12d 
 |-  ( v = x -> ( ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) <-> ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> x = w ) ) )
16 fveq2 
 |-  ( w = y -> ( ( F |` ( 1 ..^ K ) ) ` w ) = ( ( F |` ( 1 ..^ K ) ) ` y ) )
17 16 eqeq2d 
 |-  ( w = y -> ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` w ) <-> ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) ) )
18 equequ2 
 |-  ( w = y -> ( x = w <-> x = y ) )
19 17 18 imbi12d 
 |-  ( w = y -> ( ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> x = w ) <-> ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) ) )
20 15 19 rspc2va 
 |-  ( ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) /\ A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) ) -> ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) )
21 fvres 
 |-  ( x e. ( 1 ..^ K ) -> ( ( F |` ( 1 ..^ K ) ) ` x ) = ( F ` x ) )
22 21 eqcomd 
 |-  ( x e. ( 1 ..^ K ) -> ( F ` x ) = ( ( F |` ( 1 ..^ K ) ) ` x ) )
23 fvres 
 |-  ( y e. ( 1 ..^ K ) -> ( ( F |` ( 1 ..^ K ) ) ` y ) = ( F ` y ) )
24 23 eqcomd 
 |-  ( y e. ( 1 ..^ K ) -> ( F ` y ) = ( ( F |` ( 1 ..^ K ) ) ` y ) )
25 22 24 eqeqan12d 
 |-  ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) ) )
26 25 biimpd 
 |-  ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( ( F ` x ) = ( F ` y ) -> ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) ) )
27 26 imim1d 
 |-  ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
28 27 imp 
 |-  ( ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) /\ ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
29 28 2a1d 
 |-  ( ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) /\ ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) )
30 29 2a1d 
 |-  ( ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) /\ ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
31 30 expcom 
 |-  ( ( ( ( F |` ( 1 ..^ K ) ) ` x ) = ( ( F |` ( 1 ..^ K ) ) ` y ) -> x = y ) -> ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) ) )
32 20 31 syl 
 |-  ( ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) /\ A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) ) -> ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) ) )
33 32 ex 
 |-  ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) -> ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) ) ) )
34 33 pm2.43a 
 |-  ( ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) ) )
35 ianor 
 |-  ( -. ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) <-> ( -. x e. ( 1 ..^ K ) \/ -. y e. ( 1 ..^ K ) ) )
36 eqcom 
 |-  ( ( F ` x ) = ( F ` y ) <-> ( F ` y ) = ( F ` x ) )
37 injresinjlem 
 |-  ( -. x e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( y e. ( 0 ... K ) /\ x e. ( 0 ... K ) ) -> ( ( F ` y ) = ( F ` x ) -> y = x ) ) ) ) ) )
38 37 imp 
 |-  ( ( -. x e. ( 1 ..^ K ) /\ ( F ` 0 ) =/= ( F ` K ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( y e. ( 0 ... K ) /\ x e. ( 0 ... K ) ) -> ( ( F ` y ) = ( F ` x ) -> y = x ) ) ) ) )
39 38 imp41 
 |-  ( ( ( ( ( -. x e. ( 1 ..^ K ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) /\ ( y e. ( 0 ... K ) /\ x e. ( 0 ... K ) ) ) -> ( ( F ` y ) = ( F ` x ) -> y = x ) )
40 eqcom 
 |-  ( y = x <-> x = y )
41 39 40 imbitrdi 
 |-  ( ( ( ( ( -. x e. ( 1 ..^ K ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) /\ ( y e. ( 0 ... K ) /\ x e. ( 0 ... K ) ) ) -> ( ( F ` y ) = ( F ` x ) -> x = y ) )
42 36 41 biimtrid 
 |-  ( ( ( ( ( -. x e. ( 1 ..^ K ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) /\ ( y e. ( 0 ... K ) /\ x e. ( 0 ... K ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
43 42 ex 
 |-  ( ( ( ( -. x e. ( 1 ..^ K ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> ( ( y e. ( 0 ... K ) /\ x e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
44 43 ancomsd 
 |-  ( ( ( ( -. x e. ( 1 ..^ K ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
45 44 exp41 
 |-  ( -. x e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
46 injresinjlem 
 |-  ( -. y e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
47 45 46 jaoi 
 |-  ( ( -. x e. ( 1 ..^ K ) \/ -. y e. ( 1 ..^ K ) ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
48 47 a1d 
 |-  ( ( -. x e. ( 1 ..^ K ) \/ -. y e. ( 1 ..^ K ) ) -> ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) ) )
49 35 48 sylbi 
 |-  ( -. ( x e. ( 1 ..^ K ) /\ y e. ( 1 ..^ K ) ) -> ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) ) )
50 34 49 pm2.61i 
 |-  ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
51 50 imp41 
 |-  ( ( ( ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> ( ( x e. ( 0 ... K ) /\ y e. ( 0 ... K ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
52 51 ralrimivv 
 |-  ( ( ( ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ ( F : ( 0 ... K ) --> V /\ K e. NN0 ) ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) )
53 52 exp41 
 |-  ( A. v e. ( 1 ..^ K ) A. w e. ( 1 ..^ K ) ( ( ( F |` ( 1 ..^ K ) ) ` v ) = ( ( F |` ( 1 ..^ K ) ) ` w ) -> v = w ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) )
54 12 53 simplbiim 
 |-  ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) )
55 54 com13 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) )
56 55 ex 
 |-  ( F : ( 0 ... K ) --> V -> ( K e. NN0 -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
57 56 com24 
 |-  ( F : ( 0 ... K ) --> V -> ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V -> ( ( F ` 0 ) =/= ( F ` K ) -> ( K e. NN0 -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) ) )
58 57 impcom 
 |-  ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( K e. NN0 -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) ) )
59 58 imp41 
 |-  ( ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) )
60 dff13 
 |-  ( F : ( 0 ... K ) -1-1-> V <-> ( F : ( 0 ... K ) --> V /\ A. x e. ( 0 ... K ) A. y e. ( 0 ... K ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
61 11 59 60 sylanbrc 
 |-  ( ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> F : ( 0 ... K ) -1-1-> V )
62 11 biantrurd 
 |-  ( ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> ( Fun `' F <-> ( F : ( 0 ... K ) --> V /\ Fun `' F ) ) )
63 df-f1 
 |-  ( F : ( 0 ... K ) -1-1-> V <-> ( F : ( 0 ... K ) --> V /\ Fun `' F ) )
64 62 63 bitr4di 
 |-  ( ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> ( Fun `' F <-> F : ( 0 ... K ) -1-1-> V ) )
65 61 64 mpbird 
 |-  ( ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) /\ ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) ) -> Fun `' F )
66 65 ex 
 |-  ( ( ( ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V /\ F : ( 0 ... K ) --> V ) /\ ( F ` 0 ) =/= ( F ` K ) ) /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) )
67 66 exp41 
 |-  ( ( F |` ( 1 ..^ K ) ) : ( 1 ..^ K ) -1-1-> V -> ( F : ( 0 ... K ) --> V -> ( ( F ` 0 ) =/= ( F ` K ) -> ( K e. NN0 -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) ) ) ) )
68 10 67 biimtrdi 
 |-  ( F : ( 0 ... K ) --> V -> ( Fun `' ( F |` ( 1 ..^ K ) ) -> ( F : ( 0 ... K ) --> V -> ( ( F ` 0 ) =/= ( F ` K ) -> ( K e. NN0 -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) ) ) ) ) )
69 68 pm2.43a 
 |-  ( F : ( 0 ... K ) --> V -> ( Fun `' ( F |` ( 1 ..^ K ) ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( K e. NN0 -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) ) ) ) )
70 69 3imp 
 |-  ( ( F : ( 0 ... K ) --> V /\ Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F ` 0 ) =/= ( F ` K ) ) -> ( K e. NN0 -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) ) )
71 70 com12 
 |-  ( K e. NN0 -> ( ( F : ( 0 ... K ) --> V /\ Fun `' ( F |` ( 1 ..^ K ) ) /\ ( F ` 0 ) =/= ( F ` K ) ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> Fun `' F ) ) )