Theorem eedimeq

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

	Ref	Expression
Assertion	eedimeq	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → 𝑁 = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		eleei	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ )
2		eleei	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) → 𝐴 : ( 1 ... 𝑀 ) ⟶ ℝ )
3		fdm	⊢ ( 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ → dom 𝐴 = ( 1 ... 𝑁 ) )
4		fdm	⊢ ( 𝐴 : ( 1 ... 𝑀 ) ⟶ ℝ → dom 𝐴 = ( 1 ... 𝑀 ) )
5	3 4	sylan9req	⊢ ( ( 𝐴 : ( 1 ... 𝑁 ) ⟶ ℝ ∧ 𝐴 : ( 1 ... 𝑀 ) ⟶ ℝ ) → ( 1 ... 𝑁 ) = ( 1 ... 𝑀 ) )
6	1 2 5	syl2an	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → ( 1 ... 𝑁 ) = ( 1 ... 𝑀 ) )
7		eleenn	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ℕ )
8		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
9	7 8	eleqtrdi	⊢ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
11		fzopth	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( ( 1 ... 𝑁 ) = ( 1 ... 𝑀 ) ↔ ( 1 = 1 ∧ 𝑁 = 𝑀 ) ) )
12	10 11	syl	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → ( ( 1 ... 𝑁 ) = ( 1 ... 𝑀 ) ↔ ( 1 = 1 ∧ 𝑁 = 𝑀 ) ) )
13	6 12	mpbid	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → ( 1 = 1 ∧ 𝑁 = 𝑀 ) )
14	13	simprd	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑀 ) ) → 𝑁 = 𝑀 )