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)

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