Metamath Proof Explorer

Theorem injresinjlem

Description: Lemma for injresinj . (Contributed by Alexander van der Vekens, 31-Oct-2017) (Proof shortened by AV, 14-Feb-2021) (Revised by Thierry Arnoux, 23-Dec-2021)

Ref Expression
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elfznelfzo 
 |-  ( ( Y e. ( 0 ... K ) /\ -. Y e. ( 1 ..^ K ) ) -> ( Y = 0 \/ Y = K ) )
2 fvinim0ffz 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) <-> ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) ) )
3 df-nel 
 |-  ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) <-> -. ( F ` 0 ) e. ( F " ( 1 ..^ K ) ) )
4 fveq2 
 |-  ( 0 = Y -> ( F ` 0 ) = ( F ` Y ) )
5 4 eqcoms 
 |-  ( Y = 0 -> ( F ` 0 ) = ( F ` Y ) )
6 5 eleq1d 
 |-  ( Y = 0 -> ( ( F ` 0 ) e. ( F " ( 1 ..^ K ) ) <-> ( F ` Y ) e. ( F " ( 1 ..^ K ) ) ) )
7 6 notbid 
 |-  ( Y = 0 -> ( -. ( F ` 0 ) e. ( F " ( 1 ..^ K ) ) <-> -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) ) )
8 7 biimpd 
 |-  ( Y = 0 -> ( -. ( F ` 0 ) e. ( F " ( 1 ..^ K ) ) -> -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) ) )
9 ffn 
 |-  ( F : ( 0 ... K ) --> V -> F Fn ( 0 ... K ) )
10 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
11 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ K ) C_ ( 0 ..^ K ) )
12 10 11 mp1i 
 |-  ( K e. NN0 -> ( 1 ..^ K ) C_ ( 0 ..^ K ) )
13 fzossfz 
 |-  ( 0 ..^ K ) C_ ( 0 ... K )
14 12 13 sstrdi 
 |-  ( K e. NN0 -> ( 1 ..^ K ) C_ ( 0 ... K ) )
15 fvelimab 
 |-  ( ( F Fn ( 0 ... K ) /\ ( 1 ..^ K ) C_ ( 0 ... K ) ) -> ( ( F ` Y ) e. ( F " ( 1 ..^ K ) ) <-> E. z e. ( 1 ..^ K ) ( F ` z ) = ( F ` Y ) ) )
16 9 14 15 syl2an 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( F ` Y ) e. ( F " ( 1 ..^ K ) ) <-> E. z e. ( 1 ..^ K ) ( F ` z ) = ( F ` Y ) ) )
17 16 notbid 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) <-> -. E. z e. ( 1 ..^ K ) ( F ` z ) = ( F ` Y ) ) )
18 ralnex 
 |-  ( A. z e. ( 1 ..^ K ) -. ( F ` z ) = ( F ` Y ) <-> -. E. z e. ( 1 ..^ K ) ( F ` z ) = ( F ` Y ) )
19 fveqeq2 
 |-  ( z = X -> ( ( F ` z ) = ( F ` Y ) <-> ( F ` X ) = ( F ` Y ) ) )
20 19 notbid 
 |-  ( z = X -> ( -. ( F ` z ) = ( F ` Y ) <-> -. ( F ` X ) = ( F ` Y ) ) )
21 20 rspcva 
 |-  ( ( X e. ( 1 ..^ K ) /\ A. z e. ( 1 ..^ K ) -. ( F ` z ) = ( F ` Y ) ) -> -. ( F ` X ) = ( F ` Y ) )
22 pm2.21 
 |-  ( -. ( F ` X ) = ( F ` Y ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
23 22 a1d 
 |-  ( -. ( F ` X ) = ( F ` Y ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
24 23 2a1d 
 |-  ( -. ( F ` X ) = ( F ` Y ) -> ( X e. ( 0 ... K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
25 21 24 syl 
 |-  ( ( X e. ( 1 ..^ K ) /\ A. z e. ( 1 ..^ K ) -. ( F ` z ) = ( F ` Y ) ) -> ( X e. ( 0 ... K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
26 25 expcom 
 |-  ( A. z e. ( 1 ..^ K ) -. ( F ` z ) = ( F ` Y ) -> ( X e. ( 1 ..^ K ) -> ( X e. ( 0 ... K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
27 26 com24 
 |-  ( A. z e. ( 1 ..^ K ) -. ( F ` z ) = ( F ` Y ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
28 18 27 sylbir 
 |-  ( -. E. z e. ( 1 ..^ K ) ( F ` z ) = ( F ` Y ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
29 28 com12 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( -. E. z e. ( 1 ..^ K ) ( F ` z ) = ( F ` Y ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
30 17 29 sylbid 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
31 30 com12 
 |-  ( -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
32 8 31 syl6com 
 |-  ( -. ( F ` 0 ) e. ( F " ( 1 ..^ K ) ) -> ( Y = 0 -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
33 3 32 sylbi 
 |-  ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) -> ( Y = 0 -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
34 33 adantr 
 |-  ( ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) -> ( Y = 0 -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
35 34 com12 
 |-  ( Y = 0 -> ( ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
36 df-nel 
 |-  ( ( F ` K ) e/ ( F " ( 1 ..^ K ) ) <-> -. ( F ` K ) e. ( F " ( 1 ..^ K ) ) )
37 fveq2 
 |-  ( K = Y -> ( F ` K ) = ( F ` Y ) )
38 37 eqcoms 
 |-  ( Y = K -> ( F ` K ) = ( F ` Y ) )
39 38 eleq1d 
 |-  ( Y = K -> ( ( F ` K ) e. ( F " ( 1 ..^ K ) ) <-> ( F ` Y ) e. ( F " ( 1 ..^ K ) ) ) )
40 39 notbid 
 |-  ( Y = K -> ( -. ( F ` K ) e. ( F " ( 1 ..^ K ) ) <-> -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) ) )
41 40 biimpd 
 |-  ( Y = K -> ( -. ( F ` K ) e. ( F " ( 1 ..^ K ) ) -> -. ( F ` Y ) e. ( F " ( 1 ..^ K ) ) ) )
42 41 31 syl6com 
 |-  ( -. ( F ` K ) e. ( F " ( 1 ..^ K ) ) -> ( Y = K -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
43 36 42 sylbi 
 |-  ( ( F ` K ) e/ ( F " ( 1 ..^ K ) ) -> ( Y = K -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
44 43 adantl 
 |-  ( ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) -> ( Y = K -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
45 44 com12 
 |-  ( Y = K -> ( ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
46 35 45 jaoi 
 |-  ( ( Y = 0 \/ Y = K ) -> ( ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
47 46 com13 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F ` 0 ) e/ ( F " ( 1 ..^ K ) ) /\ ( F ` K ) e/ ( F " ( 1 ..^ K ) ) ) -> ( ( Y = 0 \/ Y = K ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
48 2 47 sylbid 
 |-  ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( Y = 0 \/ Y = K ) -> ( X e. ( 0 ... K ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
49 48 com14 
 |-  ( X e. ( 0 ... K ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
50 49 com12 
 |-  ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( X e. ( 0 ... K ) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( X e. ( 1 ..^ K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
51 50 com15 
 |-  ( X e. ( 1 ..^ K ) -> ( X e. ( 0 ... K ) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
52 elfznelfzo 
 |-  ( ( X e. ( 0 ... K ) /\ -. X e. ( 1 ..^ K ) ) -> ( X = 0 \/ X = K ) )
53 eqtr3 
 |-  ( ( X = 0 /\ Y = 0 ) -> X = Y )
54 2a1 
 |-  ( X = Y -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
55 54 2a1d 
 |-  ( X = Y -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
56 53 55 syl 
 |-  ( ( X = 0 /\ Y = 0 ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
57 5 adantl 
 |-  ( ( X = K /\ Y = 0 ) -> ( F ` 0 ) = ( F ` Y ) )
58 fveq2 
 |-  ( K = X -> ( F ` K ) = ( F ` X ) )
59 58 eqcoms 
 |-  ( X = K -> ( F ` K ) = ( F ` X ) )
60 59 adantr 
 |-  ( ( X = K /\ Y = 0 ) -> ( F ` K ) = ( F ` X ) )
61 57 60 neeq12d 
 |-  ( ( X = K /\ Y = 0 ) -> ( ( F ` 0 ) =/= ( F ` K ) <-> ( F ` Y ) =/= ( F ` X ) ) )
62 df-ne 
 |-  ( ( F ` Y ) =/= ( F ` X ) <-> -. ( F ` Y ) = ( F ` X ) )
63 pm2.24 
 |-  ( ( F ` Y ) = ( F ` X ) -> ( -. ( F ` Y ) = ( F ` X ) -> X = Y ) )
64 63 eqcoms 
 |-  ( ( F ` X ) = ( F ` Y ) -> ( -. ( F ` Y ) = ( F ` X ) -> X = Y ) )
65 64 com12 
 |-  ( -. ( F ` Y ) = ( F ` X ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
66 62 65 sylbi 
 |-  ( ( F ` Y ) =/= ( F ` X ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
67 61 66 syl6bi 
 |-  ( ( X = K /\ Y = 0 ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
68 67 2a1d 
 |-  ( ( X = K /\ Y = 0 ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
69 fveq2 
 |-  ( 0 = X -> ( F ` 0 ) = ( F ` X ) )
70 69 eqcoms 
 |-  ( X = 0 -> ( F ` 0 ) = ( F ` X ) )
71 70 adantr 
 |-  ( ( X = 0 /\ Y = K ) -> ( F ` 0 ) = ( F ` X ) )
72 38 adantl 
 |-  ( ( X = 0 /\ Y = K ) -> ( F ` K ) = ( F ` Y ) )
73 71 72 neeq12d 
 |-  ( ( X = 0 /\ Y = K ) -> ( ( F ` 0 ) =/= ( F ` K ) <-> ( F ` X ) =/= ( F ` Y ) ) )
74 df-ne 
 |-  ( ( F ` X ) =/= ( F ` Y ) <-> -. ( F ` X ) = ( F ` Y ) )
75 74 22 sylbi 
 |-  ( ( F ` X ) =/= ( F ` Y ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) )
76 73 75 syl6bi 
 |-  ( ( X = 0 /\ Y = K ) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) )
77 76 2a1d 
 |-  ( ( X = 0 /\ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
78 eqtr3 
 |-  ( ( X = K /\ Y = K ) -> X = Y )
79 78 55 syl 
 |-  ( ( X = K /\ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
80 56 68 77 79 ccase 
 |-  ( ( ( X = 0 \/ X = K ) /\ ( Y = 0 \/ Y = K ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) )
81 80 ex 
 |-  ( ( X = 0 \/ X = K ) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
82 52 81 syl 
 |-  ( ( X e. ( 0 ... K ) /\ -. X e. ( 1 ..^ K ) ) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
83 82 expcom 
 |-  ( -. X e. ( 1 ..^ K ) -> ( X e. ( 0 ... K ) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
84 51 83 pm2.61i 
 |-  ( X e. ( 0 ... K ) -> ( ( Y = 0 \/ Y = K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
85 84 com12 
 |-  ( ( Y = 0 \/ Y = K ) -> ( X e. ( 0 ... K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
86 1 85 syl 
 |-  ( ( Y e. ( 0 ... K ) /\ -. Y e. ( 1 ..^ K ) ) -> ( X e. ( 0 ... K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
87 86 ex 
 |-  ( Y e. ( 0 ... K ) -> ( -. Y e. ( 1 ..^ K ) -> ( X e. ( 0 ... K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
88 87 com23 
 |-  ( Y e. ( 0 ... K ) -> ( X e. ( 0 ... K ) -> ( -. Y e. ( 1 ..^ K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) ) )
89 88 impcom 
 |-  ( ( X e. ( 0 ... K ) /\ Y e. ( 0 ... K ) ) -> ( -. Y e. ( 1 ..^ K ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
90 89 com12 
 |-  ( -. Y e. ( 1 ..^ K ) -> ( ( X e. ( 0 ... K ) /\ Y e. ( 0 ... K ) ) -> ( ( F : ( 0 ... K ) --> V /\ K e. NN0 ) -> ( ( ( F " { 0 , K } ) i^i ( F " ( 1 ..^ K ) ) ) = (/) -> ( ( F ` 0 ) =/= ( F ` K ) -> ( ( F ` X ) = ( F ` Y ) -> X = Y ) ) ) ) ) )
91 90 com25 
 |-  ( -. 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 ) ) ) ) ) )