Theorem axlowdimlem10

Description: Lemma for axlowdim . Set up a family of points in Euclidean space. (Contributed by Scott Fenton, 21-Apr-2013)

	Ref	Expression
Hypothesis	axlowdimlem10.1	$$⊢Q=\left\{⟨I+1,1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right)$$
Assertion	axlowdimlem10	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to Q\in 𝔼\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		axlowdimlem10.1	$$⊢Q=\left\{⟨I+1,1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right)$$
2		ovex	$$⊢I+1\in \mathrm{V}$$
3		1ex	$$⊢1\in \mathrm{V}$$
4	2 3	f1osn	$$⊢\left\{⟨I+1,1⟩\right\}:\left\{I+1\right\}\underset{1-1\; onto}{⟶}\left\{1\right\}$$
5		f1of	$$⊢\left\{⟨I+1,1⟩\right\}:\left\{I+1\right\}\underset{1-1\; onto}{⟶}\left\{1\right\}\to \left\{⟨I+1,1⟩\right\}:\left\{I+1\right\}⟶\left\{1\right\}$$
6	4 5	ax-mp	$$⊢\left\{⟨I+1,1⟩\right\}:\left\{I+1\right\}⟶\left\{1\right\}$$
7		c0ex	$$⊢0\in \mathrm{V}$$
8	7	fconst	$$⊢\left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{I+1\right\}⟶\left\{0\right\}$$
9	6 8	pm3.2i	$$⊢\left(\left\{⟨I+1,1⟩\right\}:\left\{I+1\right\}⟶\left\{1\right\}\wedge \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{I+1\right\}⟶\left\{0\right\}\right)$$
10		disjdif	$$⊢\left\{I+1\right\}\cap \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)=\varnothing$$
11		fun	$$⊢\left(\left(\left\{⟨I+1,1⟩\right\}:\left\{I+1\right\}⟶\left\{1\right\}\wedge \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right):\left(1\dots N\right)\setminus \left\{I+1\right\}⟶\left\{0\right\}\right)\wedge \left\{I+1\right\}\cap \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)=\varnothing \right)\to \left(\left\{⟨I+1,1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right)\right):\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶\left\{1\right\}\cup \left\{0\right\}$$
12	9 10 11	mp2an	$$⊢\left(\left\{⟨I+1,1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right)\right):\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶\left\{1\right\}\cup \left\{0\right\}$$
13	1	feq1i	$$⊢Q:\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶\left\{1\right\}\cup \left\{0\right\}\leftrightarrow \left(\left\{⟨I+1,1⟩\right\}\cup \left(\left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)\times \left\{0\right\}\right)\right):\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶\left\{1\right\}\cup \left\{0\right\}$$
14	12 13	mpbir	$$⊢Q:\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶\left\{1\right\}\cup \left\{0\right\}$$
15		1re	$$⊢1\in ℝ$$
16		snssi	$$⊢1\in ℝ\to \left\{1\right\}\subseteq ℝ$$
17	15 16	ax-mp	$$⊢\left\{1\right\}\subseteq ℝ$$
18		0re	$$⊢0\in ℝ$$
19		snssi	$$⊢0\in ℝ\to \left\{0\right\}\subseteq ℝ$$
20	18 19	ax-mp	$$⊢\left\{0\right\}\subseteq ℝ$$
21	17 20	unssi	$$⊢\left\{1\right\}\cup \left\{0\right\}\subseteq ℝ$$
22		fss	$$⊢\left(Q:\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶\left\{1\right\}\cup \left\{0\right\}\wedge \left\{1\right\}\cup \left\{0\right\}\subseteq ℝ\right)\to Q:\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶ℝ$$
23	14 21 22	mp2an	$$⊢Q:\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶ℝ$$
24		fznatpl1	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to I+1\in \left(1\dots N\right)$$
25	24	snssd	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to \left\{I+1\right\}\subseteq \left(1\dots N\right)$$
26		undif	$$⊢\left\{I+1\right\}\subseteq \left(1\dots N\right)\leftrightarrow \left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)=\left(1\dots N\right)$$
27	25 26	sylib	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to \left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)=\left(1\dots N\right)$$
28	27	feq2d	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to \left(Q:\left\{I+1\right\}\cup \left(\left(1\dots N\right)\setminus \left\{I+1\right\}\right)⟶ℝ\leftrightarrow Q:\left(1\dots N\right)⟶ℝ\right)$$
29	23 28	mpbii	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to Q:\left(1\dots N\right)⟶ℝ$$
30		elee	$$⊢N\in \mathbb{N}\to \left(Q\in 𝔼\left(N\right)\leftrightarrow Q:\left(1\dots N\right)⟶ℝ\right)$$
31	30	adantr	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to \left(Q\in 𝔼\left(N\right)\leftrightarrow Q:\left(1\dots N\right)⟶ℝ\right)$$
32	29 31	mpbird	$$⊢\left(N\in \mathbb{N}\wedge I\in \left(1\dots N-1\right)\right)\to Q\in 𝔼\left(N\right)$$