axlowdimlem15

Description: Lemma for axlowdim . Set up a one-to-one function of points. (Contributed by Scott Fenton, 21-Apr-2013)

		Ref	Expression
	Hypothesis	axlowdimlem15.1	$⊢ F = (i \in (1 \dots N - 1) ⟼ if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})))$
	Assertion	axlowdimlem15	$⊢ N \in ℤ_{\geq 3} \to F : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N)$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem15.1	$⊢ F = (i \in (1 \dots N - 1) ⟼ if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})))$
2		eqid	$⊢ \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
3	2	axlowdimlem7	$⊢ N \in ℤ_{\geq 3} \to \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \in 𝔼 (N)$
4	3	adantr	$⊢ (N \in ℤ_{\geq 3} \land i \in (1 \dots N - 1)) \to \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \in 𝔼 (N)$
5		eluz3nn	$⊢ N \in ℤ_{\geq 3} \to N \in ℕ$
6		eqid	$⊢ \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) = \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})$
7	6	axlowdimlem10	$⊢ (N \in ℕ \land i \in (1 \dots N - 1)) \to \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) \in 𝔼 (N)$
8	5 7	sylan	$⊢ (N \in ℤ_{\geq 3} \land i \in (1 \dots N - 1)) \to \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) \in 𝔼 (N)$
9	4 8	ifcld	$⊢ (N \in ℤ_{\geq 3} \land i \in (1 \dots N - 1)) \to if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})) \in 𝔼 (N)$
10	9 1	fmptd	$⊢ N \in ℤ_{\geq 3} \to F : (1 \dots N - 1) ⟶ 𝔼 (N)$
11		eqeq1	$⊢ i = j \to (i = 1 \leftrightarrow j = 1)$
12		oveq1	$⊢ i = j \to i + 1 = j + 1$
13	12	opeq1d	$⊢ i = j \to ⟨i + 1, 1⟩ = ⟨j + 1, 1⟩$
14	13	sneqd	$⊢ i = j \to \{⟨i + 1, 1⟩\} = \{⟨j + 1, 1⟩\}$
15	12	sneqd	$⊢ i = j \to \{i + 1\} = \{j + 1\}$
16	15	difeq2d	$⊢ i = j \to (1 \dots N) ∖ \{i + 1\} = (1 \dots N) ∖ \{j + 1\}$
17	16	xpeq1d	$⊢ i = j \to ((1 \dots N) ∖ \{i + 1\}) \times \{0\} = ((1 \dots N) ∖ \{j + 1\}) \times \{0\}$
18	14 17	uneq12d	$⊢ i = j \to \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) = \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})$
19	11 18	ifbieq2d	$⊢ i = j \to if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})) = if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}))$
20		snex	$⊢ \{⟨3, - 1⟩\} \in V$
21		ovex	$⊢ (1 \dots N) \in V$
22	21	difexi	$⊢ (1 \dots N) ∖ \{3\} \in V$
23		snex	$⊢ \{0\} \in V$
24	22 23	xpex	$⊢ ((1 \dots N) ∖ \{3\}) \times \{0\} \in V$
25	20 24	unex	$⊢ \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \in V$
26		snex	$⊢ \{⟨j + 1, 1⟩\} \in V$
27	21	difexi	$⊢ (1 \dots N) ∖ \{j + 1\} \in V$
28	27 23	xpex	$⊢ ((1 \dots N) ∖ \{j + 1\}) \times \{0\} \in V$
29	26 28	unex	$⊢ \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) \in V$
30	25 29	ifex	$⊢ if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) \in V$
31	19 1 30	fvmpt	$⊢ j \in (1 \dots N - 1) \to F (j) = if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}))$
32		eqeq1	$⊢ i = k \to (i = 1 \leftrightarrow k = 1)$
33		oveq1	$⊢ i = k \to i + 1 = k + 1$
34	33	opeq1d	$⊢ i = k \to ⟨i + 1, 1⟩ = ⟨k + 1, 1⟩$
35	34	sneqd	$⊢ i = k \to \{⟨i + 1, 1⟩\} = \{⟨k + 1, 1⟩\}$
36	33	sneqd	$⊢ i = k \to \{i + 1\} = \{k + 1\}$
37	36	difeq2d	$⊢ i = k \to (1 \dots N) ∖ \{i + 1\} = (1 \dots N) ∖ \{k + 1\}$
38	37	xpeq1d	$⊢ i = k \to ((1 \dots N) ∖ \{i + 1\}) \times \{0\} = ((1 \dots N) ∖ \{k + 1\}) \times \{0\}$
39	35 38	uneq12d	$⊢ i = k \to \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})$
40	32 39	ifbieq2d	$⊢ i = k \to if (i = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨i + 1, 1⟩\} \cup (((1 \dots N) ∖ \{i + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))$
41		snex	$⊢ \{⟨k + 1, 1⟩\} \in V$
42	21	difexi	$⊢ (1 \dots N) ∖ \{k + 1\} \in V$
43	42 23	xpex	$⊢ ((1 \dots N) ∖ \{k + 1\}) \times \{0\} \in V$
44	41 43	unex	$⊢ \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \in V$
45	25 44	ifex	$⊢ if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \in V$
46	40 1 45	fvmpt	$⊢ k \in (1 \dots N - 1) \to F (k) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))$
47	31 46	eqeqan12d	$⊢ (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1)) \to (F (j) = F (k) \leftrightarrow if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})))$
48	47	adantl	$⊢ (N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (F (j) = F (k) \leftrightarrow if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})))$
49		eqtr3	$⊢ (j = 1 \land k = 1) \to j = k$
50	49	2a1d	$⊢ (j = 1 \land k = 1) \to ((N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k))$
51		eqid	$⊢ \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})$
52	2 51	axlowdimlem13	$⊢ (N \in ℕ \land k \in (1 \dots N - 1)) \to \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \neq \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})$
53	52	neneqd	$⊢ (N \in ℕ \land k \in (1 \dots N - 1)) \to \neg \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})$
54	53	pm2.21d	$⊢ (N \in ℕ \land k \in (1 \dots N - 1)) \to (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k)$
55	54	adantrl	$⊢ (N \in ℕ \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k)$
56	5 55	sylan	$⊢ (N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k)$
57		iftrue	$⊢ j = 1 \to if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
58		iffalse	$⊢ \neg k = 1 \to if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})$
59	57 58	eqeqan12d	$⊢ (j = 1 \land \neg k = 1) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \leftrightarrow \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))$
60	59	imbi1d	$⊢ (j = 1 \land \neg k = 1) \to ((if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k) \leftrightarrow (\{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k))$
61	56 60	imbitrrid	$⊢ (j = 1 \land \neg k = 1) \to ((N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k))$
62		eqid	$⊢ \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})$
63	2 62	axlowdimlem13	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \neq \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})$
64	63	necomd	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) \neq \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
65	64	neneqd	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to \neg \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
66	65	pm2.21d	$⊢ (N \in ℕ \land j \in (1 \dots N - 1)) \to (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \to j = k)$
67	5 66	sylan	$⊢ (N \in ℤ_{\geq 3} \land j \in (1 \dots N - 1)) \to (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \to j = k)$
68	67	adantrr	$⊢ (N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \to j = k)$
69		iffalse	$⊢ \neg j = 1 \to if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})$
70		iftrue	$⊢ k = 1 \to if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\})$
71	69 70	eqeqan12d	$⊢ (\neg j = 1 \land k = 1) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \leftrightarrow \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}))$
72	71	imbi1d	$⊢ (\neg j = 1 \land k = 1) \to ((if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k) \leftrightarrow (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}) \to j = k))$
73	68 72	imbitrrid	$⊢ (\neg j = 1 \land k = 1) \to ((N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k))$
74	62 51	axlowdimlem14	$⊢ (N \in ℕ \land j \in (1 \dots N - 1) \land k \in (1 \dots N - 1)) \to (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k)$
75	74	3expb	$⊢ (N \in ℕ \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k)$
76	5 75	sylan	$⊢ (N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k)$
77	69 58	eqeqan12d	$⊢ (\neg j = 1 \land \neg k = 1) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \leftrightarrow \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}))$
78	77	imbi1d	$⊢ (\neg j = 1 \land \neg k = 1) \to ((if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k) \leftrightarrow (\{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\}) = \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\}) \to j = k))$
79	76 78	imbitrrid	$⊢ (\neg j = 1 \land \neg k = 1) \to ((N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k))$
80	50 61 73 79	4cases	$⊢ (N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (if (j = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨j + 1, 1⟩\} \cup (((1 \dots N) ∖ \{j + 1\}) \times \{0\})) = if (k = 1, \{⟨3, - 1⟩\} \cup (((1 \dots N) ∖ \{3\}) \times \{0\}), \{⟨k + 1, 1⟩\} \cup (((1 \dots N) ∖ \{k + 1\}) \times \{0\})) \to j = k)$
81	48 80	sylbid	$⊢ (N \in ℤ_{\geq 3} \land (j \in (1 \dots N - 1) \land k \in (1 \dots N - 1))) \to (F (j) = F (k) \to j = k)$
82	81	ralrimivva	$⊢ N \in ℤ_{\geq 3} \to \forall j \in (1 \dots N - 1) \forall k \in (1 \dots N - 1) (F (j) = F (k) \to j = k)$
83		dff13	$⊢ F : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N) \leftrightarrow (F : (1 \dots N - 1) ⟶ 𝔼 (N) \land \forall j \in (1 \dots N - 1) \forall k \in (1 \dots N - 1) (F (j) = F (k) \to j = k))$
84	10 82 83	sylanbrc	$⊢ N \in ℤ_{\geq 3} \to F : (1 \dots N - 1) \underset{1-1}{⟶} 𝔼 (N)$

Metamath Proof Explorer

Theorem axlowdimlem15

Proof