Metamath Proof Explorer

Theorem f1resfz0f1d

Description: If a function with a sequence of nonnegative integers (starting at 0) as its domain is one-to-one when 0 is removed, and if the range of that restriction does not contain the function's value at the removed integer, then the function is itself one-to-one. (Contributed by BTernaryTau, 4-Oct-2023) (Revised by Mingli Yuan, 15-Aug-2026)

Ref Expression
Hypotheses f1resfz0f1d.1 
|- ( ph -> K e. NN0 )
f1resfz0f1d.2 
|- ( ph -> F : ( 0 ... K ) --> V )
f1resfz0f1d.3 
|- ( ph -> Fun `' ( F |` ( 1 ... K ) ) )
f1resfz0f1d.4 
|- ( ph -> ( ( F " { 0 } ) i^i ( F " ( 1 ... K ) ) ) = (/) )
Assertion f1resfz0f1d 
|- ( ph -> F : ( 0 ... K ) -1-1-> V )

Proof

Step Hyp Ref Expression
1 f1resfz0f1d.1 
 |-  ( ph -> K e. NN0 )
2 f1resfz0f1d.2 
 |-  ( ph -> F : ( 0 ... K ) --> V )
3 f1resfz0f1d.3 
 |-  ( ph -> Fun `' ( F |` ( 1 ... K ) ) )
4 f1resfz0f1d.4 
 |-  ( ph -> ( ( F " { 0 } ) i^i ( F " ( 1 ... K ) ) ) = (/) )
5 fz1ssfz0 
 |-  ( 1 ... K ) C_ ( 0 ... K )
6 5 a1i 
 |-  ( ph -> ( 1 ... K ) C_ ( 0 ... K ) )
7 2 6 fssresd 
 |-  ( ph -> ( F |` ( 1 ... K ) ) : ( 1 ... K ) --> V )
8 df-f1 
 |-  ( ( F |` ( 1 ... K ) ) : ( 1 ... K ) -1-1-> V <-> ( ( F |` ( 1 ... K ) ) : ( 1 ... K ) --> V /\ Fun `' ( F |` ( 1 ... K ) ) ) )
9 8 a1i 
 |-  ( ph -> ( ( F |` ( 1 ... K ) ) : ( 1 ... K ) -1-1-> V <-> ( ( F |` ( 1 ... K ) ) : ( 1 ... K ) --> V /\ Fun `' ( F |` ( 1 ... K ) ) ) ) )
10 7 3 9 mpbir2and 
 |-  ( ph -> ( F |` ( 1 ... K ) ) : ( 1 ... K ) -1-1-> V )
11 0elfz 
 |-  ( K e. NN0 -> 0 e. ( 0 ... K ) )
12 snssi 
 |-  ( 0 e. ( 0 ... K ) -> { 0 } C_ ( 0 ... K ) )
13 1 11 12 3syl 
 |-  ( ph -> { 0 } C_ ( 0 ... K ) )
14 2 13 fssresd 
 |-  ( ph -> ( F |` { 0 } ) : { 0 } --> V )
15 eqidd 
 |-  ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` 0 ) -> 0 = 0 )
16 0nn0 
 |-  0 e. NN0
17 fveqeq2 
 |-  ( x = 0 -> ( ( ( F |` { 0 } ) ` x ) = ( ( F |` { 0 } ) ` y ) <-> ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` y ) ) )
18 eqeq1 
 |-  ( x = 0 -> ( x = y <-> 0 = y ) )
19 17 18 imbi12d 
 |-  ( x = 0 -> ( ( ( ( F |` { 0 } ) ` x ) = ( ( F |` { 0 } ) ` y ) -> x = y ) <-> ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` y ) -> 0 = y ) ) )
20 fveq2 
 |-  ( y = 0 -> ( ( F |` { 0 } ) ` y ) = ( ( F |` { 0 } ) ` 0 ) )
21 20 eqeq2d 
 |-  ( y = 0 -> ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` y ) <-> ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` 0 ) ) )
22 eqeq2 
 |-  ( y = 0 -> ( 0 = y <-> 0 = 0 ) )
23 21 22 imbi12d 
 |-  ( y = 0 -> ( ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` y ) -> 0 = y ) <-> ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` 0 ) -> 0 = 0 ) ) )
24 19 23 2ralsng 
 |-  ( ( 0 e. NN0 /\ 0 e. NN0 ) -> ( A. x e. { 0 } A. y e. { 0 } ( ( ( F |` { 0 } ) ` x ) = ( ( F |` { 0 } ) ` y ) -> x = y ) <-> ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` 0 ) -> 0 = 0 ) ) )
25 16 16 24 mp2an 
 |-  ( A. x e. { 0 } A. y e. { 0 } ( ( ( F |` { 0 } ) ` x ) = ( ( F |` { 0 } ) ` y ) -> x = y ) <-> ( ( ( F |` { 0 } ) ` 0 ) = ( ( F |` { 0 } ) ` 0 ) -> 0 = 0 ) )
26 15 25 mpbir 
 |-  A. x e. { 0 } A. y e. { 0 } ( ( ( F |` { 0 } ) ` x ) = ( ( F |` { 0 } ) ` y ) -> x = y )
27 dff13 
 |-  ( ( F |` { 0 } ) : { 0 } -1-1-> V <-> ( ( F |` { 0 } ) : { 0 } --> V /\ A. x e. { 0 } A. y e. { 0 } ( ( ( F |` { 0 } ) ` x ) = ( ( F |` { 0 } ) ` y ) -> x = y ) ) )
28 14 26 27 sylanblrc 
 |-  ( ph -> ( F |` { 0 } ) : { 0 } -1-1-> V )
29 uncom 
 |-  ( ( 1 ... K ) u. { 0 } ) = ( { 0 } u. ( 1 ... K ) )
30 fz0sn0fz1 
 |-  ( K e. NN0 -> ( 0 ... K ) = ( { 0 } u. ( 1 ... K ) ) )
31 1 30 syl 
 |-  ( ph -> ( 0 ... K ) = ( { 0 } u. ( 1 ... K ) ) )
32 29 31 eqtr4id 
 |-  ( ph -> ( ( 1 ... K ) u. { 0 } ) = ( 0 ... K ) )
33 0nelfz1 
 |-  0 e/ ( 1 ... K )
34 33 neli 
 |-  -. 0 e. ( 1 ... K )
35 disjsn 
 |-  ( ( ( 1 ... K ) i^i { 0 } ) = (/) <-> -. 0 e. ( 1 ... K ) )
36 34 35 mpbir 
 |-  ( ( 1 ... K ) i^i { 0 } ) = (/)
37 uneqdifeq 
 |-  ( ( ( 1 ... K ) C_ ( 0 ... K ) /\ ( ( 1 ... K ) i^i { 0 } ) = (/) ) -> ( ( ( 1 ... K ) u. { 0 } ) = ( 0 ... K ) <-> ( ( 0 ... K ) \ ( 1 ... K ) ) = { 0 } ) )
38 5 36 37 mp2an 
 |-  ( ( ( 1 ... K ) u. { 0 } ) = ( 0 ... K ) <-> ( ( 0 ... K ) \ ( 1 ... K ) ) = { 0 } )
39 32 38 sylib 
 |-  ( ph -> ( ( 0 ... K ) \ ( 1 ... K ) ) = { 0 } )
40 39 eqcomd 
 |-  ( ph -> { 0 } = ( ( 0 ... K ) \ ( 1 ... K ) ) )
41 40 reseq2d 
 |-  ( ph -> ( F |` { 0 } ) = ( F |` ( ( 0 ... K ) \ ( 1 ... K ) ) ) )
42 eqidd 
 |-  ( ph -> V = V )
43 41 40 42 f1eq123d 
 |-  ( ph -> ( ( F |` { 0 } ) : { 0 } -1-1-> V <-> ( F |` ( ( 0 ... K ) \ ( 1 ... K ) ) ) : ( ( 0 ... K ) \ ( 1 ... K ) ) -1-1-> V ) )
44 28 43 mpbid 
 |-  ( ph -> ( F |` ( ( 0 ... K ) \ ( 1 ... K ) ) ) : ( ( 0 ... K ) \ ( 1 ... K ) ) -1-1-> V )
45 40 imaeq2d 
 |-  ( ph -> ( F " { 0 } ) = ( F " ( ( 0 ... K ) \ ( 1 ... K ) ) ) )
46 45 ineq2d 
 |-  ( ph -> ( ( F " ( 1 ... K ) ) i^i ( F " { 0 } ) ) = ( ( F " ( 1 ... K ) ) i^i ( F " ( ( 0 ... K ) \ ( 1 ... K ) ) ) ) )
47 incom 
 |-  ( ( F " { 0 } ) i^i ( F " ( 1 ... K ) ) ) = ( ( F " ( 1 ... K ) ) i^i ( F " { 0 } ) )
48 47 4 eqtr3id 
 |-  ( ph -> ( ( F " ( 1 ... K ) ) i^i ( F " { 0 } ) ) = (/) )
49 46 48 eqtr3d 
 |-  ( ph -> ( ( F " ( 1 ... K ) ) i^i ( F " ( ( 0 ... K ) \ ( 1 ... K ) ) ) ) = (/) )
50 6 2 10 44 49 f1resrcmplf1d 
 |-  ( ph -> F : ( 0 ... K ) -1-1-> V )