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	$$⊢\neg Y\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(\left(X\in \left(0\dots K\right)\wedge Y\in \left(0\dots K\right)\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfznelfzo	$$⊢\left(Y\in \left(0\dots K\right)\wedge \neg Y\in \left(1..^K\right)\right)\to \left(Y=0\vee Y=K\right)$$
2		fvinim0ffz	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \leftrightarrow \left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\right)$$
3		df-nel	$$⊢F\left(0\right)\notin F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(0\right)\in F\left[\left(1..^K\right)\right]$$
4		fveq2	$$⊢0=Y\to F\left(0\right)=F\left(Y\right)$$
5	4	eqcoms	$$⊢Y=0\to F\left(0\right)=F\left(Y\right)$$
6	5	eleq1d	$$⊢Y=0\to \left(F\left(0\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow F\left(Y\right)\in F\left[\left(1..^K\right)\right]\right)$$
7	6	notbid	$$⊢Y=0\to \left(\neg F\left(0\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\right)$$
8	7	biimpd	$$⊢Y=0\to \left(\neg F\left(0\right)\in F\left[\left(1..^K\right)\right]\to \neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\right)$$
9		ffn	$$⊢F:\left(0\dots K\right)⟶V\to FFn\left(0\dots K\right)$$
10		1eluzge0	$$⊢1\in {\mathbb{Z}}_{\ge 0}$$
11		fzoss1	$$⊢1\in {\mathbb{Z}}_{\ge 0}\to \left(1..^K\right)\subseteq \left(0..^K\right)$$
12	10 11	mp1i	$$⊢K\in {\mathbb{N}}_0\to \left(1..^K\right)\subseteq \left(0..^K\right)$$
13		fzossfz	$$⊢\left(0..^K\right)\subseteq \left(0\dots K\right)$$
14	12 13	sstrdi	$$⊢K\in {\mathbb{N}}_0\to \left(1..^K\right)\subseteq \left(0\dots K\right)$$
15		fvelimab	$$⊢\left(FFn\left(0\dots K\right)\wedge \left(1..^K\right)\subseteq \left(0\dots K\right)\right)\to \left(F\left(Y\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow \exists z\in \left(1..^K\right)F\left(z\right)=F\left(Y\right)\right)$$
16	9 14 15	syl2an	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left(Y\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow \exists z\in \left(1..^K\right)F\left(z\right)=F\left(Y\right)\right)$$
17	16	notbid	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(\neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow \neg \exists z\in \left(1..^K\right)F\left(z\right)=F\left(Y\right)\right)$$
18		ralnex	$$⊢\forall z\in \left(1..^K\right)\neg F\left(z\right)=F\left(Y\right)\leftrightarrow \neg \exists z\in \left(1..^K\right)F\left(z\right)=F\left(Y\right)$$
19		fveqeq2	$$⊢z=X\to \left(F\left(z\right)=F\left(Y\right)\leftrightarrow F\left(X\right)=F\left(Y\right)\right)$$
20	19	notbid	$$⊢z=X\to \left(\neg F\left(z\right)=F\left(Y\right)\leftrightarrow \neg F\left(X\right)=F\left(Y\right)\right)$$
21	20	rspcva	$$⊢\left(X\in \left(1..^K\right)\wedge \forall z\in \left(1..^K\right)\neg F\left(z\right)=F\left(Y\right)\right)\to \neg F\left(X\right)=F\left(Y\right)$$
22		pm2.21	$$⊢\neg F\left(X\right)=F\left(Y\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
23	22	a1d	$$⊢\neg F\left(X\right)=F\left(Y\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
24	23	2a1d	$$⊢\neg F\left(X\right)=F\left(Y\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
25	21 24	syl	$$⊢\left(X\in \left(1..^K\right)\wedge \forall z\in \left(1..^K\right)\neg F\left(z\right)=F\left(Y\right)\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
26	25	expcom	$$⊢\forall z\in \left(1..^K\right)\neg F\left(z\right)=F\left(Y\right)\to \left(X\in \left(1..^K\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
27	26	com24	$$⊢\forall z\in \left(1..^K\right)\neg F\left(z\right)=F\left(Y\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
28	18 27	sylbir	$$⊢\neg \exists z\in \left(1..^K\right)F\left(z\right)=F\left(Y\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
29	28	com12	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(\neg \exists z\in \left(1..^K\right)F\left(z\right)=F\left(Y\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
30	17 29	sylbid	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(\neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
31	30	com12	$$⊢\neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
32	8 31	syl6com	$$⊢\neg F\left(0\right)\in F\left[\left(1..^K\right)\right]\to \left(Y=0\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
33	3 32	sylbi	$$⊢F\left(0\right)\notin F\left[\left(1..^K\right)\right]\to \left(Y=0\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
34	33	adantr	$$⊢\left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\to \left(Y=0\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
35	34	com12	$$⊢Y=0\to \left(\left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
36		df-nel	$$⊢F\left(K\right)\notin F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(K\right)\in F\left[\left(1..^K\right)\right]$$
37		fveq2	$$⊢K=Y\to F\left(K\right)=F\left(Y\right)$$
38	37	eqcoms	$$⊢Y=K\to F\left(K\right)=F\left(Y\right)$$
39	38	eleq1d	$$⊢Y=K\to \left(F\left(K\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow F\left(Y\right)\in F\left[\left(1..^K\right)\right]\right)$$
40	39	notbid	$$⊢Y=K\to \left(\neg F\left(K\right)\in F\left[\left(1..^K\right)\right]\leftrightarrow \neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\right)$$
41	40	biimpd	$$⊢Y=K\to \left(\neg F\left(K\right)\in F\left[\left(1..^K\right)\right]\to \neg F\left(Y\right)\in F\left[\left(1..^K\right)\right]\right)$$
42	41 31	syl6com	$$⊢\neg F\left(K\right)\in F\left[\left(1..^K\right)\right]\to \left(Y=K\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
43	36 42	sylbi	$$⊢F\left(K\right)\notin F\left[\left(1..^K\right)\right]\to \left(Y=K\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
44	43	adantl	$$⊢\left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\to \left(Y=K\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
45	44	com12	$$⊢Y=K\to \left(\left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
46	35 45	jaoi	$$⊢\left(Y=0\vee Y=K\right)\to \left(\left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
47	46	com13	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(\left(F\left(0\right)\notin F\left[\left(1..^K\right)\right]\wedge F\left(K\right)\notin F\left[\left(1..^K\right)\right]\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
48	2 47	sylbid	$$⊢\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(\left(Y=0\vee Y=K\right)\to \left(X\in \left(0\dots K\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
49	48	com14	$$⊢X\in \left(0\dots K\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
50	49	com12	$$⊢F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(X\in \left(0\dots K\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(X\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
51	50	com15	$$⊢X\in \left(1..^K\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
52		elfznelfzo	$$⊢\left(X\in \left(0\dots K\right)\wedge \neg X\in \left(1..^K\right)\right)\to \left(X=0\vee X=K\right)$$
53		eqtr3	$$⊢\left(X=0\wedge Y=0\right)\to X=Y$$
54		2a1	$$⊢X=Y\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
55	54	2a1d	$$⊢X=Y\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
56	53 55	syl	$$⊢\left(X=0\wedge Y=0\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
57	5	adantl	$$⊢\left(X=K\wedge Y=0\right)\to F\left(0\right)=F\left(Y\right)$$
58		fveq2	$$⊢K=X\to F\left(K\right)=F\left(X\right)$$
59	58	eqcoms	$$⊢X=K\to F\left(K\right)=F\left(X\right)$$
60	59	adantr	$$⊢\left(X=K\wedge Y=0\right)\to F\left(K\right)=F\left(X\right)$$
61	57 60	neeq12d	$$⊢\left(X=K\wedge Y=0\right)\to \left(F\left(0\right)\ne F\left(K\right)\leftrightarrow F\left(Y\right)\ne F\left(X\right)\right)$$
62		df-ne	$$⊢F\left(Y\right)\ne F\left(X\right)\leftrightarrow \neg F\left(Y\right)=F\left(X\right)$$
63		pm2.24	$$⊢F\left(Y\right)=F\left(X\right)\to \left(\neg F\left(Y\right)=F\left(X\right)\to X=Y\right)$$
64	63	eqcoms	$$⊢F\left(X\right)=F\left(Y\right)\to \left(\neg F\left(Y\right)=F\left(X\right)\to X=Y\right)$$
65	64	com12	$$⊢\neg F\left(Y\right)=F\left(X\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
66	62 65	sylbi	$$⊢F\left(Y\right)\ne F\left(X\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
67	61 66	syl6bi	$$⊢\left(X=K\wedge Y=0\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
68	67	2a1d	$$⊢\left(X=K\wedge Y=0\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
69		fveq2	$$⊢0=X\to F\left(0\right)=F\left(X\right)$$
70	69	eqcoms	$$⊢X=0\to F\left(0\right)=F\left(X\right)$$
71	70	adantr	$$⊢\left(X=0\wedge Y=K\right)\to F\left(0\right)=F\left(X\right)$$
72	38	adantl	$$⊢\left(X=0\wedge Y=K\right)\to F\left(K\right)=F\left(Y\right)$$
73	71 72	neeq12d	$$⊢\left(X=0\wedge Y=K\right)\to \left(F\left(0\right)\ne F\left(K\right)\leftrightarrow F\left(X\right)\ne F\left(Y\right)\right)$$
74		df-ne	$$⊢F\left(X\right)\ne F\left(Y\right)\leftrightarrow \neg F\left(X\right)=F\left(Y\right)$$
75	74 22	sylbi	$$⊢F\left(X\right)\ne F\left(Y\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)$$
76	73 75	syl6bi	$$⊢\left(X=0\wedge Y=K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)$$
77	76	2a1d	$$⊢\left(X=0\wedge Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
78		eqtr3	$$⊢\left(X=K\wedge Y=K\right)\to X=Y$$
79	78 55	syl	$$⊢\left(X=K\wedge Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
80	56 68 77 79	ccase	$$⊢\left(\left(X=0\vee X=K\right)\wedge \left(Y=0\vee Y=K\right)\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)$$
81	80	ex	$$⊢\left(X=0\vee X=K\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
82	52 81	syl	$$⊢\left(X\in \left(0\dots K\right)\wedge \neg X\in \left(1..^K\right)\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
83	82	expcom	$$⊢\neg X\in \left(1..^K\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
84	51 83	pm2.61i	$$⊢X\in \left(0\dots K\right)\to \left(\left(Y=0\vee Y=K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
85	84	com12	$$⊢\left(Y=0\vee Y=K\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
86	1 85	syl	$$⊢\left(Y\in \left(0\dots K\right)\wedge \neg Y\in \left(1..^K\right)\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
87	86	ex	$$⊢Y\in \left(0\dots K\right)\to \left(\neg Y\in \left(1..^K\right)\to \left(X\in \left(0\dots K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
88	87	com23	$$⊢Y\in \left(0\dots K\right)\to \left(X\in \left(0\dots K\right)\to \left(\neg Y\in \left(1..^K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)\right)$$
89	88	impcom	$$⊢\left(X\in \left(0\dots K\right)\wedge Y\in \left(0\dots K\right)\right)\to \left(\neg Y\in \left(1..^K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
90	89	com12	$$⊢\neg Y\in \left(1..^K\right)\to \left(\left(X\in \left(0\dots K\right)\wedge Y\in \left(0\dots K\right)\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(F\left(0\right)\ne F\left(K\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$
91	90	com25	$$⊢\neg Y\in \left(1..^K\right)\to \left(F\left(0\right)\ne F\left(K\right)\to \left(\left(F:\left(0\dots K\right)⟶V\wedge K\in {\mathbb{N}}_0\right)\to \left(F\left[\left\{0,K\right\}\right]\cap F\left[\left(1..^K\right)\right]=\varnothing \to \left(\left(X\in \left(0\dots K\right)\wedge Y\in \left(0\dots K\right)\right)\to \left(F\left(X\right)=F\left(Y\right)\to X=Y\right)\right)\right)\right)\right)$$