Theorem axlowdimlem7

Description: Lemma for axlowdim . Set up a point in Euclidean space. (Contributed by Scott Fenton, 29-Jun-2013)

	Ref	Expression
Hypothesis	axlowdimlem7.1	$$⊢P=\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)$$
Assertion	axlowdimlem7	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P\in 𝔼\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem7.1	$$⊢P=\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)$$
2		eqid	$$⊢\left\{⟨3,-1⟩\right\}=\left\{⟨3,-1⟩\right\}$$
3		3ex	$$⊢3\in \mathrm{V}$$
4		negex	$$⊢-1\in \mathrm{V}$$
5	3 4	fsn	$$⊢\left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶\left\{-1\right\}\leftrightarrow \left\{⟨3,-1⟩\right\}=\left\{⟨3,-1⟩\right\}$$
6	2 5	mpbir	$$⊢\left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶\left\{-1\right\}$$
7		neg1rr	$$⊢-1\in ℝ$$
8		snssi	$$⊢-1\in ℝ\to \left\{-1\right\}\subseteq ℝ$$
9	7 8	ax-mp	$$⊢\left\{-1\right\}\subseteq ℝ$$
10		fss	$$⊢\left(\left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶\left\{-1\right\}\wedge \left\{-1\right\}\subseteq ℝ\right)\to \left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶ℝ$$
11	6 9 10	mp2an	$$⊢\left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶ℝ$$
12		0re	$$⊢0\in ℝ$$
13	12	fconst6	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶ℝ$$
14	11 13	pm3.2i	$$⊢\left(\left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶ℝ\wedge \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶ℝ\right)$$
15		disjdif	$$⊢\left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing$$
16		fun2	$$⊢\left(\left(\left\{⟨3,-1⟩\right\}:\left\{3\right\}⟶ℝ\wedge \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{3\right\}⟶ℝ\right)\wedge \left\{3\right\}\cap \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\varnothing \right)\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left\{3\right\}\cup \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)⟶ℝ$$
17	14 15 16	mp2an	$$⊢\left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left\{3\right\}\cup \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)⟶ℝ$$
18		eluzle	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\le N$$
19		1le3	$$⊢1\le 3$$
20	18 19	jctil	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(1\le 3\wedge 3\le N\right)$$
21		3z	$$⊢3\in \mathbb{Z}$$
22		1z	$$⊢1\in \mathbb{Z}$$
23		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{Z}$$
24		elfz	$$⊢\left(3\in \mathbb{Z}\wedge 1\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(3\in \left(1\dots N\right)\leftrightarrow \left(1\le 3\wedge 3\le N\right)\right)$$
25	21 22 23 24	mp3an12i	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(3\in \left(1\dots N\right)\leftrightarrow \left(1\le 3\wedge 3\le N\right)\right)$$
26	20 25	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to 3\in \left(1\dots N\right)$$
27	26	snssd	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{3\right\}\subseteq \left(1\dots N\right)$$
28		undif	$$⊢\left\{3\right\}\subseteq \left(1\dots N\right)\leftrightarrow \left\{3\right\}\cup \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\left(1\dots N\right)$$
29	27 28	sylib	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{3\right\}\cup \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)=\left(1\dots N\right)$$
30	29	feq2d	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left\{3\right\}\cup \left(\left(1\dots N\right)\setminus \left\{3\right\}\right)⟶ℝ\leftrightarrow \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left(1\dots N\right)⟶ℝ\right)$$
31	17 30	mpbii	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left(1\dots N\right)⟶ℝ$$
32		eluz3nn	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to N\in \mathbb{N}$$
33		elee	$$⊢N\in \mathbb{N}\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\in 𝔼\left(N\right)\leftrightarrow \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left(1\dots N\right)⟶ℝ\right)$$
34	32 33	syl	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\in 𝔼\left(N\right)\leftrightarrow \left(\left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\right):\left(1\dots N\right)⟶ℝ\right)$$
35	31 34	mpbird	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to \left\{⟨3,-1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{3\right\}\right)\times \left\{0\right\}\right)\in 𝔼\left(N\right)$$
36	1 35	eqeltrid	$$⊢N\in {\mathbb{Z}}_{\ge 3}\to P\in 𝔼\left(N\right)$$