Theorem axdimuniq

Description: The unique dimension axiom. If a point is in N dimensional space and in M dimensional space, then N = M . This axiom is not traditionally presented with Tarski's axioms, but we require it here as we are considering spaces in arbitrary dimensions. (Contributed by Scott Fenton, 24-Sep-2013)

	Ref	Expression
Assertion	axdimuniq	$$⊢\left(\left(N\in \mathbb{N}\wedge A\in 𝔼\left(N\right)\right)\wedge \left(M\in \mathbb{N}\wedge A\in 𝔼\left(M\right)\right)\right)\to N=M$$

Proof

Step	Hyp	Ref	Expression
1		eedimeq	$$⊢\left(A\in 𝔼\left(N\right)\wedge A\in 𝔼\left(M\right)\right)\to N=M$$
2	1	ad2ant2l	$$⊢\left(\left(N\in \mathbb{N}\wedge A\in 𝔼\left(N\right)\right)\wedge \left(M\in \mathbb{N}\wedge A\in 𝔼\left(M\right)\right)\right)\to N=M$$