Metamath Proof Explorer

Theorem eedimeq

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

Ref Expression
Assertion eedimeq 
|- ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> N = M )

Proof

Step Hyp Ref Expression
1 eleei 
 |-  ( A e. ( EE ` N ) -> A : ( 1 ... N ) --> RR )
2 eleei 
 |-  ( A e. ( EE ` M ) -> A : ( 1 ... M ) --> RR )
3 fdm 
 |-  ( A : ( 1 ... N ) --> RR -> dom A = ( 1 ... N ) )
4 fdm 
 |-  ( A : ( 1 ... M ) --> RR -> dom A = ( 1 ... M ) )
5 3 4 sylan9req 
 |-  ( ( A : ( 1 ... N ) --> RR /\ A : ( 1 ... M ) --> RR ) -> ( 1 ... N ) = ( 1 ... M ) )
6 1 2 5 syl2an 
 |-  ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> ( 1 ... N ) = ( 1 ... M ) )
7 eleenn 
 |-  ( A e. ( EE ` N ) -> N e. NN )
8 nnuz 
 |-  NN = ( ZZ>= ` 1 )
9 7 8 eleqtrdi 
 |-  ( A e. ( EE ` N ) -> N e. ( ZZ>= ` 1 ) )
10 9 adantr 
 |-  ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> N e. ( ZZ>= ` 1 ) )
11 fzopth 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ( 1 ... N ) = ( 1 ... M ) <-> ( 1 = 1 /\ N = M ) ) )
12 10 11 syl 
 |-  ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> ( ( 1 ... N ) = ( 1 ... M ) <-> ( 1 = 1 /\ N = M ) ) )
13 6 12 mpbid 
 |-  ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> ( 1 = 1 /\ N = M ) )
14 13 simprd 
 |-  ( ( A e. ( EE ` N ) /\ A e. ( EE ` M ) ) -> N = M )