Theorem axlowdimlem15 25636

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

Hypothesis

Ref	Expression
axlowdimlem15.1	⊢ 𝐹 = (𝑖 ∈ (1...(𝑁 − 1)) ↦ if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))))

Assertion

Ref	Expression
axlowdimlem15	⊢ (𝑁 ∈ (ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁))

Distinct variable group:   𝑖,𝑁

Allowed substitution hint:   𝐹(𝑖)

Proof of Theorem axlowdimlem15

Dummy variables 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2610	. . . . . 6 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))
2	1	axlowdimlem7 25628	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘3) → ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈ (𝔼‘𝑁))
3	2	adantr 480	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈ (𝔼‘𝑁))
4		eluzge3nn 11606	. . . . 5 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝑁 ∈ ℕ)
5		eqid 2610	. . . . . 6 ⊢ ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))
6	5	axlowdimlem10 25631	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈ (𝔼‘𝑁))
7	4, 6	sylan 487	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) ∈ (𝔼‘𝑁))
8	3, 7	ifcld 4081	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑖 ∈ (1...(𝑁 − 1))) → if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) ∈ (𝔼‘𝑁))
9		axlowdimlem15.1	. . 3 ⊢ 𝐹 = (𝑖 ∈ (1...(𝑁 − 1)) ↦ if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))))
10	8, 9	fmptd 6292	. 2 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁))
11		eqeq1 2614	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → (𝑖 = 1 ↔ 𝑗 = 1))
12		oveq1 6556	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → (𝑖 + 1) = (𝑗 + 1))
13	12	opeq1d 4346	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → ⟨(𝑖 + 1), 1⟩ = ⟨(𝑗 + 1), 1⟩)
14	13	sneqd 4137	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → {⟨(𝑖 + 1), 1⟩} = {⟨(𝑗 + 1), 1⟩})
15	12	sneqd 4137	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑗 → {(𝑖 + 1)} = {(𝑗 + 1)})
16	15	difeq2d 3690	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑗 + 1)}))
17	16	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑖 = 𝑗 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))
18	14, 17	uneq12d 3730	. . . . . . . 8 ⊢ (𝑖 = 𝑗 → ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})))
19	11, 18	ifbieq2d 4061	. . . . . . 7 ⊢ (𝑖 = 𝑗 → if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) = if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))))
20		snex 4835	. . . . . . . . 9 ⊢ {⟨3, -1⟩} ∈ V
21		ovex 6577	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ V
22		difexg 4735	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {3}) ∈ V)
23	21, 22	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ {3}) ∈ V
24		snex 4835	. . . . . . . . . 10 ⊢ {0} ∈ V
25	23, 24	xpex 6860	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ {3}) × {0}) ∈ V
26	20, 25	unex 6854	. . . . . . . 8 ⊢ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ∈ V
27		snex 4835	. . . . . . . . 9 ⊢ {⟨(𝑗 + 1), 1⟩} ∈ V
28		difexg 4735	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(𝑗 + 1)}) ∈ V)
29	21, 28	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ {(𝑗 + 1)}) ∈ V
30	29, 24	xpex 6860	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}) ∈ V
31	27, 30	unex 6854	. . . . . . . 8 ⊢ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) ∈ V
32	26, 31	ifex 4106	. . . . . . 7 ⊢ if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) ∈ V
33	19, 9, 32	fvmpt 6191	. . . . . 6 ⊢ (𝑗 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑗) = if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))))
34		eqeq1 2614	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → (𝑖 = 1 ↔ 𝑘 = 1))
35		oveq1 6556	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1))
36	35	opeq1d 4346	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → ⟨(𝑖 + 1), 1⟩ = ⟨(𝑘 + 1), 1⟩)
37	36	sneqd 4137	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → {⟨(𝑖 + 1), 1⟩} = {⟨(𝑘 + 1), 1⟩})
38	35	sneqd 4137	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑘 → {(𝑖 + 1)} = {(𝑘 + 1)})
39	38	difeq2d 3690	. . . . . . . . . 10 ⊢ (𝑖 = 𝑘 → ((1...𝑁) ∖ {(𝑖 + 1)}) = ((1...𝑁) ∖ {(𝑘 + 1)}))
40	39	xpeq1d 5062	. . . . . . . . 9 ⊢ (𝑖 = 𝑘 → (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}) = (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))
41	37, 40	uneq12d 3730	. . . . . . . 8 ⊢ (𝑖 = 𝑘 → ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))
42	34, 41	ifbieq2d 4061	. . . . . . 7 ⊢ (𝑖 = 𝑘 → if(𝑖 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑖 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑖 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))
43		snex 4835	. . . . . . . . 9 ⊢ {⟨(𝑘 + 1), 1⟩} ∈ V
44		difexg 4735	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∈ V → ((1...𝑁) ∖ {(𝑘 + 1)}) ∈ V)
45	21, 44	ax-mp 5	. . . . . . . . . 10 ⊢ ((1...𝑁) ∖ {(𝑘 + 1)}) ∈ V
46	45, 24	xpex 6860	. . . . . . . . 9 ⊢ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}) ∈ V
47	43, 46	unex 6854	. . . . . . . 8 ⊢ ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) ∈ V
48	26, 47	ifex 4106	. . . . . . 7 ⊢ if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ∈ V
49	42, 9, 48	fvmpt 6191	. . . . . 6 ⊢ (𝑘 ∈ (1...(𝑁 − 1)) → (𝐹‘𝑘) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))
50	33, 49	eqeqan12d 2626	. . . . 5 ⊢ ((𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ((𝐹‘𝑗) = (𝐹‘𝑘) ↔ if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))))
51	50	adantl 481	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → ((𝐹‘𝑗) = (𝐹‘𝑘) ↔ if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))))
52		eqtr3 2631	. . . . . 6 ⊢ ((𝑗 = 1 ∧ 𝑘 = 1) → 𝑗 = 𝑘)
53	52	2a1d 26	. . . . 5 ⊢ ((𝑗 = 1 ∧ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘)))
54		eqid 2610	. . . . . . . . . . 11 ⊢ ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))
55	1, 54	axlowdimlem13 25634	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ≠ ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))
56	55	neneqd 2787	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → ¬ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))
57	56	pm2.21d 117	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))
58	57	adantrl 748	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))
59	4, 58	sylan 487	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))
60		iftrue 4042	. . . . . . . 8 ⊢ (𝑗 = 1 → if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})))
61		iffalse 4045	. . . . . . . 8 ⊢ (¬ 𝑘 = 1 → if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})))
62	60, 61	eqeqan12d 2626	. . . . . . 7 ⊢ ((𝑗 = 1 ∧ ¬ 𝑘 = 1) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ↔ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))
63	62	imbi1d 330	. . . . . 6 ⊢ ((𝑗 = 1 ∧ ¬ 𝑘 = 1) → ((if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘) ↔ (({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)))
64	59, 63	syl5ibr 235	. . . . 5 ⊢ ((𝑗 = 1 ∧ ¬ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘)))
65		eqid 2610	. . . . . . . . . . . 12 ⊢ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))
66	1, 65	axlowdimlem13 25634	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) ≠ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})))
67	66	necomd 2837	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) ≠ ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})))
68	67	neneqd 2787	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → ¬ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})))
69	68	pm2.21d 117	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘))
70	4, 69	sylan 487	. . . . . . 7 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑗 ∈ (1...(𝑁 − 1))) → (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘))
71	70	adantrr 749	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘))
72		iffalse 4045	. . . . . . . 8 ⊢ (¬ 𝑗 = 1 → if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})))
73		iftrue 4042	. . . . . . . 8 ⊢ (𝑘 = 1 → if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})))
74	72, 73	eqeqan12d 2626	. . . . . . 7 ⊢ ((¬ 𝑗 = 1 ∧ 𝑘 = 1) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ↔ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0}))))
75	74	imbi1d 330	. . . . . 6 ⊢ ((¬ 𝑗 = 1 ∧ 𝑘 = 1) → ((if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘) ↔ (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})) → 𝑗 = 𝑘)))
76	71, 75	syl5ibr 235	. . . . 5 ⊢ ((¬ 𝑗 = 1 ∧ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘)))
77	65, 54	axlowdimlem14 25635	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1))) → (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))
78	77	3expb 1258	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))
79	4, 78	sylan 487	. . . . . 6 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘))
80	72, 61	eqeqan12d 2626	. . . . . . 7 ⊢ ((¬ 𝑗 = 1 ∧ ¬ 𝑘 = 1) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) ↔ ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))))
81	80	imbi1d 330	. . . . . 6 ⊢ ((¬ 𝑗 = 1 ∧ ¬ 𝑘 = 1) → ((if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘) ↔ (({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0})) = ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0})) → 𝑗 = 𝑘)))
82	79, 81	syl5ibr 235	. . . . 5 ⊢ ((¬ 𝑗 = 1 ∧ ¬ 𝑘 = 1) → ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘)))
83	53, 64, 76, 82	4cases 987	. . . 4 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → (if(𝑗 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑗 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑗 + 1)}) × {0}))) = if(𝑘 = 1, ({⟨3, -1⟩} ∪ (((1...𝑁) ∖ {3}) × {0})), ({⟨(𝑘 + 1), 1⟩} ∪ (((1...𝑁) ∖ {(𝑘 + 1)}) × {0}))) → 𝑗 = 𝑘))
84	51, 83	sylbid 229	. . 3 ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (𝑗 ∈ (1...(𝑁 − 1)) ∧ 𝑘 ∈ (1...(𝑁 − 1)))) → ((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘))
85	84	ralrimivva 2954	. 2 ⊢ (𝑁 ∈ (ℤ≥‘3) → ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘))
86		dff13 6416	. 2 ⊢ (𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁) ↔ (𝐹:(1...(𝑁 − 1))⟶(𝔼‘𝑁) ∧ ∀𝑗 ∈ (1...(𝑁 − 1))∀𝑘 ∈ (1...(𝑁 − 1))((𝐹‘𝑗) = (𝐹‘𝑘) → 𝑗 = 𝑘)))
87	10, 85, 86	sylanbrc 695	1 ⊢ (𝑁 ∈ (ℤ≥‘3) → 𝐹:(1...(𝑁 − 1))–1-1→(𝔼‘𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538  ifcif 4036  {csn 4125  ⟨cop 4131   ↦ cmpt 4643   × cxp 5036  ⟶wf 5800  –1-1→wf1 5801  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818   − cmin 10145  -cneg 10146  ℕcn 10897  3c3 10948  ℤ_≥cuz 11563  ...cfz 12197  𝔼cee 25568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-ee 25571

This theorem is referenced by:  axlowdim  25641