eedimeq

Description: A point belongs to at most one Euclidean space. (Contributed by Scott Fenton, 1-Jul-2013)

		Ref	Expression
	Assertion	eedimeq	$⊢ (A \in 𝔼 (N) \land A \in 𝔼 (M)) \to N = M$

Step	Hyp	Ref	Expression
1		eleei	$⊢ A \in 𝔼 (N) \to A : (1 \dots N) ⟶ ℝ$
2		eleei	$⊢ A \in 𝔼 (M) \to A : (1 \dots M) ⟶ ℝ$
3		fdm	$⊢ A : (1 \dots N) ⟶ ℝ \to dom A = (1 \dots N)$
4		fdm	$⊢ A : (1 \dots M) ⟶ ℝ \to dom A = (1 \dots M)$
5	3 4	sylan9req	$⊢ (A : (1 \dots N) ⟶ ℝ \land A : (1 \dots M) ⟶ ℝ) \to (1 \dots N) = (1 \dots M)$
6	1 2 5	syl2an	$⊢ (A \in 𝔼 (N) \land A \in 𝔼 (M)) \to (1 \dots N) = (1 \dots M)$
7		eleenn	$⊢ A \in 𝔼 (N) \to N \in ℕ$
8		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
9	7 8	eleqtrdi	$⊢ A \in 𝔼 (N) \to N \in ℤ_{\geq 1}$
10	9	adantr	$⊢ (A \in 𝔼 (N) \land A \in 𝔼 (M)) \to N \in ℤ_{\geq 1}$
11		fzopth	$⊢ N \in ℤ_{\geq 1} \to ((1 \dots N) = (1 \dots M) \leftrightarrow (1 = 1 \land N = M))$
12	10 11	syl	$⊢ (A \in 𝔼 (N) \land A \in 𝔼 (M)) \to ((1 \dots N) = (1 \dots M) \leftrightarrow (1 = 1 \land N = M))$
13	6 12	mpbid	$⊢ (A \in 𝔼 (N) \land A \in 𝔼 (M)) \to (1 = 1 \land N = M)$
14	13	simprd	$⊢ (A \in 𝔼 (N) \land A \in 𝔼 (M)) \to N = M$

Metamath Proof Explorer