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 \in ℕ_{0} \to ((F : (0 \dots K) ⟶ V \land Fun {({F ↾}_{(1 ..^K)})}^{-1} \land F (0) \neq F (K)) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		fzo0ss1	$⊢ (1 ..^K) \subseteq (0 ..^K)$
2		fzossfz	$⊢ (0 ..^K) \subseteq (0 \dots K)$
3	1 2	sstri	$⊢ (1 ..^K) \subseteq (0 \dots K)$
4		fssres	$⊢ (F : (0 \dots K) ⟶ V \land (1 ..^K) \subseteq (0 \dots K)) \to ({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V$
5	3 4	mpan2	$⊢ F : (0 \dots K) ⟶ V \to ({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V$
6	5	biantrud	$⊢ F : (0 \dots K) ⟶ V \to (Fun {({F ↾}_{(1 ..^K)})}^{-1} \leftrightarrow (Fun {({F ↾}_{(1 ..^K)})}^{-1} \land ({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V))$
7		ancom	$⊢ (Fun {({F ↾}_{(1 ..^K)})}^{-1} \land ({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V) \leftrightarrow (({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V \land Fun {({F ↾}_{(1 ..^K)})}^{-1})$
8		df-f1	$⊢ ({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \leftrightarrow (({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V \land Fun {({F ↾}_{(1 ..^K)})}^{-1})$
9	7 8	bitr4i	$⊢ (Fun {({F ↾}_{(1 ..^K)})}^{-1} \land ({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V) \leftrightarrow ({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V$
10	6 9	bitrdi	$⊢ F : (0 \dots K) ⟶ V \to (Fun {({F ↾}_{(1 ..^K)})}^{-1} \leftrightarrow ({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V)$
11		simp-4r	$⊢ ((((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to F : (0 \dots K) ⟶ V$
12		dff13	$⊢ ({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \leftrightarrow (({F ↾}_{(1 ..^K)}) : (1 ..^K) ⟶ V \land \forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w))$
13		fveqeq2	$⊢ v = x \to (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \leftrightarrow ({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (w))$
14		equequ1	$⊢ v = x \to (v = w \leftrightarrow x = w)$
15	13 14	imbi12d	$⊢ v = x \to ((({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \leftrightarrow (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (w) \to x = w))$
16		fveq2	$⊢ w = y \to ({F ↾}_{(1 ..^K)}) (w) = ({F ↾}_{(1 ..^K)}) (y)$
17	16	eqeq2d	$⊢ w = y \to (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (w) \leftrightarrow ({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y))$
18		equequ2	$⊢ w = y \to (x = w \leftrightarrow x = y)$
19	17 18	imbi12d	$⊢ w = y \to ((({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (w) \to x = w) \leftrightarrow (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y))$
20	15 19	rspc2va	$⊢ ((x \in (1 ..^K) \land y \in (1 ..^K)) \land \forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w)) \to (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y)$
21		fvres	$⊢ x \in (1 ..^K) \to ({F ↾}_{(1 ..^K)}) (x) = F (x)$
22	21	eqcomd	$⊢ x \in (1 ..^K) \to F (x) = ({F ↾}_{(1 ..^K)}) (x)$
23		fvres	$⊢ y \in (1 ..^K) \to ({F ↾}_{(1 ..^K)}) (y) = F (y)$
24	23	eqcomd	$⊢ y \in (1 ..^K) \to F (y) = ({F ↾}_{(1 ..^K)}) (y)$
25	22 24	eqeqan12d	$⊢ (x \in (1 ..^K) \land y \in (1 ..^K)) \to (F (x) = F (y) \leftrightarrow ({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y))$
26	25	biimpd	$⊢ (x \in (1 ..^K) \land y \in (1 ..^K)) \to (F (x) = F (y) \to ({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y))$
27	26	imim1d	$⊢ (x \in (1 ..^K) \land y \in (1 ..^K)) \to ((({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y) \to (F (x) = F (y) \to x = y))$
28	27	imp	$⊢ ((x \in (1 ..^K) \land y \in (1 ..^K)) \land (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y)) \to (F (x) = F (y) \to x = y)$
29	28	2a1d	$⊢ ((x \in (1 ..^K) \land y \in (1 ..^K)) \land (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y)) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))$
30	29	2a1d	$⊢ ((x \in (1 ..^K) \land y \in (1 ..^K)) \land (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y)) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))))$
31	30	expcom	$⊢ (({F ↾}_{(1 ..^K)}) (x) = ({F ↾}_{(1 ..^K)}) (y) \to x = y) \to ((x \in (1 ..^K) \land y \in (1 ..^K)) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))))))$
32	20 31	syl	$⊢ ((x \in (1 ..^K) \land y \in (1 ..^K)) \land \forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w)) \to ((x \in (1 ..^K) \land y \in (1 ..^K)) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))))))$
33	32	ex	$⊢ (x \in (1 ..^K) \land y \in (1 ..^K)) \to (\forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \to ((x \in (1 ..^K) \land y \in (1 ..^K)) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))))))$
34	33	pm2.43a	$⊢ (x \in (1 ..^K) \land y \in (1 ..^K)) \to (\forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))))))$
35		ianor	$⊢ \neg (x \in (1 ..^K) \land y \in (1 ..^K)) \leftrightarrow (\neg x \in (1 ..^K) \lor \neg y \in (1 ..^K))$
36		eqcom	$⊢ F (x) = F (y) \leftrightarrow F (y) = F (x)$
37		injresinjlem	$⊢ \neg x \in (1 ..^K) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((y \in (0 \dots K) \land x \in (0 \dots K)) \to (F (y) = F (x) \to y = x)))))$
38	37	imp	$⊢ (\neg x \in (1 ..^K) \land F (0) \neq F (K)) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((y \in (0 \dots K) \land x \in (0 \dots K)) \to (F (y) = F (x) \to y = x))))$
39	38	imp41	$⊢ ((((\neg x \in (1 ..^K) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \land (y \in (0 \dots K) \land x \in (0 \dots K))) \to (F (y) = F (x) \to y = x)$
40		eqcom	$⊢ y = x \leftrightarrow x = y$
41	39 40	syl6ib	$⊢ ((((\neg x \in (1 ..^K) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \land (y \in (0 \dots K) \land x \in (0 \dots K))) \to (F (y) = F (x) \to x = y)$
42	36 41	syl5bi	$⊢ ((((\neg x \in (1 ..^K) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \land (y \in (0 \dots K) \land x \in (0 \dots K))) \to (F (x) = F (y) \to x = y)$
43	42	ex	$⊢ (((\neg x \in (1 ..^K) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to ((y \in (0 \dots K) \land x \in (0 \dots K)) \to (F (x) = F (y) \to x = y))$
44	43	ancomsd	$⊢ (((\neg x \in (1 ..^K) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))$
45	44	exp41	$⊢ \neg x \in (1 ..^K) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))))$
46		injresinjlem	$⊢ \neg y \in (1 ..^K) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))))$
47	45 46	jaoi	$⊢ (\neg x \in (1 ..^K) \lor \neg y \in (1 ..^K)) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))))$
48	47	a1d	$⊢ (\neg x \in (1 ..^K) \lor \neg y \in (1 ..^K)) \to (\forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))))))$
49	35 48	sylbi	$⊢ \neg (x \in (1 ..^K) \land y \in (1 ..^K)) \to (\forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))))))$
50	34 49	pm2.61i	$⊢ \forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y)))))$
51	50	imp41	$⊢ (((\forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to ((x \in (0 \dots K) \land y \in (0 \dots K)) \to (F (x) = F (y) \to x = y))$
52	51	ralrimivv	$⊢ (((\forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \land F (0) \neq F (K)) \land (F : (0 \dots K) ⟶ V \land K \in ℕ_{0})) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y)$
53	52	exp41	$⊢ \forall v \in (1 ..^K) \forall w \in (1 ..^K) (({F ↾}_{(1 ..^K)}) (v) = ({F ↾}_{(1 ..^K)}) (w) \to v = w) \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y))))$
54	12 53	simplbiim	$⊢ ({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \to (F (0) \neq F (K) \to ((F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y))))$
55	54	com13	$⊢ (F : (0 \dots K) ⟶ V \land K \in ℕ_{0}) \to (F (0) \neq F (K) \to (({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y))))$
56	55	ex	$⊢ F : (0 \dots K) ⟶ V \to (K \in ℕ_{0} \to (F (0) \neq F (K) \to (({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y)))))$
57	56	com24	$⊢ F : (0 \dots K) ⟶ V \to (({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \to (F (0) \neq F (K) \to (K \in ℕ_{0} \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y)))))$
58	57	impcom	$⊢ (({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \to (F (0) \neq F (K) \to (K \in ℕ_{0} \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y))))$
59	58	imp41	$⊢ ((((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y)$
60		dff13	$⊢ F : (0 \dots K) \underset{1-1}{⟶} V \leftrightarrow (F : (0 \dots K) ⟶ V \land \forall x \in (0 \dots K) \forall y \in (0 \dots K) (F (x) = F (y) \to x = y))$
61	11 59 60	sylanbrc	$⊢ ((((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to F : (0 \dots K) \underset{1-1}{⟶} V$
62	11	biantrurd	$⊢ ((((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to (Fun F^{-1} \leftrightarrow (F : (0 \dots K) ⟶ V \land Fun F^{-1}))$
63		df-f1	$⊢ F : (0 \dots K) \underset{1-1}{⟶} V \leftrightarrow (F : (0 \dots K) ⟶ V \land Fun F^{-1})$
64	62 63	bitr4di	$⊢ ((((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to (Fun F^{-1} \leftrightarrow F : (0 \dots K) \underset{1-1}{⟶} V)$
65	61 64	mpbird	$⊢ ((((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \land F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset) \to Fun F^{-1}$
66	65	ex	$⊢ (((({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \land F : (0 \dots K) ⟶ V) \land F (0) \neq F (K)) \land K \in ℕ_{0}) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1})$
67	66	exp41	$⊢ ({F ↾}_{(1 ..^K)}) : (1 ..^K) \underset{1-1}{⟶} V \to (F : (0 \dots K) ⟶ V \to (F (0) \neq F (K) \to (K \in ℕ_{0} \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1}))))$
68	10 67	syl6bi	$⊢ F : (0 \dots K) ⟶ V \to (Fun {({F ↾}_{(1 ..^K)})}^{-1} \to (F : (0 \dots K) ⟶ V \to (F (0) \neq F (K) \to (K \in ℕ_{0} \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1})))))$
69	68	pm2.43a	$⊢ F : (0 \dots K) ⟶ V \to (Fun {({F ↾}_{(1 ..^K)})}^{-1} \to (F (0) \neq F (K) \to (K \in ℕ_{0} \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1}))))$
70	69	3imp	$⊢ (F : (0 \dots K) ⟶ V \land Fun {({F ↾}_{(1 ..^K)})}^{-1} \land F (0) \neq F (K)) \to (K \in ℕ_{0} \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1}))$
71	70	com12	$⊢ K \in ℕ_{0} \to ((F : (0 \dots K) ⟶ V \land Fun {({F ↾}_{(1 ..^K)})}^{-1} \land F (0) \neq F (K)) \to (F [\{0, K\}] \cap F [(1 ..^K)] = \emptyset \to Fun F^{-1}))$

Metamath Proof Explorer

Theorem injresinj

Proof