Theorem axlowdim1

Description: The lower dimension axiom for one dimension. In any dimension, there are at least two distinct points. Theorem 3.13 of Schwabhauser p. 32, where it is derived from axlowdim2 . (Contributed by Scott Fenton, 22-Apr-2013)

	Ref	Expression
Assertion	axlowdim1	$$⊢N\in \mathbb{N}\to \exists x\in 𝔼\left(N\right)\exists y\in 𝔼\left(N\right)x\ne y$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2	1	fconst6	$$⊢\left(\left(1\dots N\right)\times \left\{1\right\}\right):\left(1\dots N\right)⟶ℝ$$
3		elee	$$⊢N\in \mathbb{N}\to \left(\left(1\dots N\right)\times \left\{1\right\}\in 𝔼\left(N\right)\leftrightarrow \left(\left(1\dots N\right)\times \left\{1\right\}\right):\left(1\dots N\right)⟶ℝ\right)$$
4	2 3	mpbiri	$$⊢N\in \mathbb{N}\to \left(1\dots N\right)\times \left\{1\right\}\in 𝔼\left(N\right)$$
5		0re	$$⊢0\in ℝ$$
6	5	fconst6	$$⊢\left(\left(1\dots N\right)\times \left\{0\right\}\right):\left(1\dots N\right)⟶ℝ$$
7		elee	$$⊢N\in \mathbb{N}\to \left(\left(1\dots N\right)\times \left\{0\right\}\in 𝔼\left(N\right)\leftrightarrow \left(\left(1\dots N\right)\times \left\{0\right\}\right):\left(1\dots N\right)⟶ℝ\right)$$
8	6 7	mpbiri	$$⊢N\in \mathbb{N}\to \left(1\dots N\right)\times \left\{0\right\}\in 𝔼\left(N\right)$$
9		ax-1ne0	$$⊢1\ne 0$$
10	9	neii	$$⊢\neg 1=0$$
11		1ex	$$⊢1\in \mathrm{V}$$
12	11	sneqr	$$⊢\left\{1\right\}=\left\{0\right\}\to 1=0$$
13	10 12	mto	$$⊢\neg \left\{1\right\}=\left\{0\right\}$$
14		elnnuz	$$⊢N\in \mathbb{N}\leftrightarrow N\in {\mathbb{Z}}_{\ge 1}$$
15		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots N\right)$$
16	14 15	sylbi	$$⊢N\in \mathbb{N}\to 1\in \left(1\dots N\right)$$
17	16	ne0d	$$⊢N\in \mathbb{N}\to \left(1\dots N\right)\ne \varnothing$$
18		rnxp	$$⊢\left(1\dots N\right)\ne \varnothing \to \mathrm{ran}\left(\left(1\dots N\right)\times \left\{1\right\}\right)=\left\{1\right\}$$
19	17 18	syl	$$⊢N\in \mathbb{N}\to \mathrm{ran}\left(\left(1\dots N\right)\times \left\{1\right\}\right)=\left\{1\right\}$$
20		rnxp	$$⊢\left(1\dots N\right)\ne \varnothing \to \mathrm{ran}\left(\left(1\dots N\right)\times \left\{0\right\}\right)=\left\{0\right\}$$
21	17 20	syl	$$⊢N\in \mathbb{N}\to \mathrm{ran}\left(\left(1\dots N\right)\times \left\{0\right\}\right)=\left\{0\right\}$$
22	19 21	eqeq12d	$$⊢N\in \mathbb{N}\to \left(\mathrm{ran}\left(\left(1\dots N\right)\times \left\{1\right\}\right)=\mathrm{ran}\left(\left(1\dots N\right)\times \left\{0\right\}\right)\leftrightarrow \left\{1\right\}=\left\{0\right\}\right)$$
23	13 22	mtbiri	$$⊢N\in \mathbb{N}\to \neg \mathrm{ran}\left(\left(1\dots N\right)\times \left\{1\right\}\right)=\mathrm{ran}\left(\left(1\dots N\right)\times \left\{0\right\}\right)$$
24		rneq	$$⊢\left(1\dots N\right)\times \left\{1\right\}=\left(1\dots N\right)\times \left\{0\right\}\to \mathrm{ran}\left(\left(1\dots N\right)\times \left\{1\right\}\right)=\mathrm{ran}\left(\left(1\dots N\right)\times \left\{0\right\}\right)$$
25	23 24	nsyl	$$⊢N\in \mathbb{N}\to \neg \left(1\dots N\right)\times \left\{1\right\}=\left(1\dots N\right)\times \left\{0\right\}$$
26	25	neqned	$$⊢N\in \mathbb{N}\to \left(1\dots N\right)\times \left\{1\right\}\ne \left(1\dots N\right)\times \left\{0\right\}$$
27		neeq1	$$⊢x=\left(1\dots N\right)\times \left\{1\right\}\to \left(x\ne y\leftrightarrow \left(1\dots N\right)\times \left\{1\right\}\ne y\right)$$
28		neeq2	$$⊢y=\left(1\dots N\right)\times \left\{0\right\}\to \left(\left(1\dots N\right)\times \left\{1\right\}\ne y\leftrightarrow \left(1\dots N\right)\times \left\{1\right\}\ne \left(1\dots N\right)\times \left\{0\right\}\right)$$
29	27 28	rspc2ev	$$⊢\left(\left(1\dots N\right)\times \left\{1\right\}\in 𝔼\left(N\right)\wedge \left(1\dots N\right)\times \left\{0\right\}\in 𝔼\left(N\right)\wedge \left(1\dots N\right)\times \left\{1\right\}\ne \left(1\dots N\right)\times \left\{0\right\}\right)\to \exists x\in 𝔼\left(N\right)\exists y\in 𝔼\left(N\right)x\ne y$$
30	4 8 26 29	syl3anc	$$⊢N\in \mathbb{N}\to \exists x\in 𝔼\left(N\right)\exists y\in 𝔼\left(N\right)x\ne y$$