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 0 F : 0 K V Fun F 1 ..^ K -1 F 0 F K F 0 K F 1 ..^ K = Fun F -1

Proof

Step Hyp Ref Expression
1 fzo0ss1 1 ..^ K 0 ..^ K
2 fzossfz 0 ..^ K 0 K
3 1 2 sstri 1 ..^ K 0 K
4 fssres F : 0 K V 1 ..^ K 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 -1 Fun F 1 ..^ K -1 F 1 ..^ K : 1 ..^ K V
7 ancom Fun F 1 ..^ K -1 F 1 ..^ K : 1 ..^ K V F 1 ..^ K : 1 ..^ K V Fun F 1 ..^ K -1
8 df-f1 F 1 ..^ K : 1 ..^ K 1-1 V F 1 ..^ K : 1 ..^ K V Fun F 1 ..^ K -1
9 7 8 bitr4i Fun F 1 ..^ K -1 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 -1 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 0 F 0 K F 1 ..^ K = F : 0 K V
12 dff13 F 1 ..^ K : 1 ..^ K 1-1 V F 1 ..^ K : 1 ..^ K V v 1 ..^ K w 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 1 ..^ K y 1 ..^ K v 1 ..^ K w 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 1 ..^ K F 1 ..^ K x = F x
22 21 eqcomd x 1 ..^ K F x = F 1 ..^ K x
23 fvres y 1 ..^ K F 1 ..^ K y = F y
24 23 eqcomd y 1 ..^ K F y = F 1 ..^ K y
25 22 24 eqeqan12d x 1 ..^ K y 1 ..^ K F x = F y F 1 ..^ K x = F 1 ..^ K y
26 25 biimpd x 1 ..^ K y 1 ..^ K F x = F y F 1 ..^ K x = F 1 ..^ K y
27 26 imim1d x 1 ..^ K y 1 ..^ K F 1 ..^ K x = F 1 ..^ K y x = y F x = F y x = y
28 27 imp x 1 ..^ K y 1 ..^ K F 1 ..^ K x = F 1 ..^ K y x = y F x = F y x = y
29 28 2a1d x 1 ..^ K y 1 ..^ K F 1 ..^ K x = F 1 ..^ K y x = y F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
30 29 2a1d x 1 ..^ K y 1 ..^ K F 1 ..^ K x = F 1 ..^ K y x = y F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
31 30 expcom F 1 ..^ K x = F 1 ..^ K y x = y x 1 ..^ K y 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
32 20 31 syl x 1 ..^ K y 1 ..^ K v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w x 1 ..^ K y 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
33 32 ex x 1 ..^ K y 1 ..^ K v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w x 1 ..^ K y 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
34 33 pm2.43a x 1 ..^ K y 1 ..^ K v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
35 ianor ¬ x 1 ..^ K y 1 ..^ K ¬ x 1 ..^ K ¬ y 1 ..^ K
36 eqcom F x = F y F y = F x
37 injresinjlem ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = y 0 K x 0 K F y = F x y = x
38 37 imp ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = y 0 K x 0 K F y = F x y = x
39 38 imp41 ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = y 0 K x 0 K F y = F x y = x
40 eqcom y = x x = y
41 39 40 syl6ib ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = y 0 K x 0 K F y = F x x = y
42 36 41 syl5bi ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = y 0 K x 0 K F x = F y x = y
43 42 ex ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = y 0 K x 0 K F x = F y x = y
44 43 ancomsd ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
45 44 exp41 ¬ x 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
46 injresinjlem ¬ y 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
47 45 46 jaoi ¬ x 1 ..^ K ¬ y 1 ..^ K F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
48 47 a1d ¬ x 1 ..^ K ¬ y 1 ..^ K v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
49 35 48 sylbi ¬ x 1 ..^ K y 1 ..^ K v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
50 34 49 pm2.61i v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
51 50 imp41 v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
52 51 ralrimivv v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
53 52 exp41 v 1 ..^ K w 1 ..^ K F 1 ..^ K v = F 1 ..^ K w v = w F 0 F K F : 0 K V K 0 F 0 K F 1 ..^ K = x 0 K y 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 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
55 54 com13 F : 0 K V K 0 F 0 F K F 1 ..^ K : 1 ..^ K 1-1 V F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
56 55 ex F : 0 K V K 0 F 0 F K F 1 ..^ K : 1 ..^ K 1-1 V F 0 K F 1 ..^ K = x 0 K y 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 0 F 0 K F 1 ..^ K = x 0 K y 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 0 F 0 K F 1 ..^ K = x 0 K y 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 0 F 0 K F 1 ..^ K = x 0 K y 0 K F x = F y x = y
60 dff13 F : 0 K 1-1 V F : 0 K V x 0 K y 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 0 F 0 K 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 0 F 0 K F 1 ..^ K = Fun F -1 F : 0 K V Fun F -1
63 df-f1 F : 0 K 1-1 V F : 0 K V Fun F -1
64 62 63 bitr4di F 1 ..^ K : 1 ..^ K 1-1 V F : 0 K V F 0 F K K 0 F 0 K F 1 ..^ K = Fun F -1 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 0 F 0 K F 1 ..^ K = Fun F -1
66 65 ex F 1 ..^ K : 1 ..^ K 1-1 V F : 0 K V F 0 F K K 0 F 0 K F 1 ..^ K = Fun F -1
67 66 exp41 F 1 ..^ K : 1 ..^ K 1-1 V F : 0 K V F 0 F K K 0 F 0 K F 1 ..^ K = Fun F -1
68 10 67 syl6bi F : 0 K V Fun F 1 ..^ K -1 F : 0 K V F 0 F K K 0 F 0 K F 1 ..^ K = Fun F -1
69 68 pm2.43a F : 0 K V Fun F 1 ..^ K -1 F 0 F K K 0 F 0 K F 1 ..^ K = Fun F -1
70 69 3imp F : 0 K V Fun F 1 ..^ K -1 F 0 F K K 0 F 0 K F 1 ..^ K = Fun F -1
71 70 com12 K 0 F : 0 K V Fun F 1 ..^ K -1 F 0 F K F 0 K F 1 ..^ K = Fun F -1