Metamath Proof Explorer


Theorem tgldim0eq

Description: In dimension zero, any two points are equal. (Contributed by Thierry Arnoux, 11-Apr-2019)

Ref Expression
Hypotheses tgldim0.g
|- P = ( E ` F )
tgldim0.p
|- ( ph -> ( # ` P ) = 1 )
tgldim0.a
|- ( ph -> A e. P )
tgldim0.b
|- ( ph -> B e. P )
Assertion tgldim0eq
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 tgldim0.g
 |-  P = ( E ` F )
2 tgldim0.p
 |-  ( ph -> ( # ` P ) = 1 )
3 tgldim0.a
 |-  ( ph -> A e. P )
4 tgldim0.b
 |-  ( ph -> B e. P )
5 1 fvexi
 |-  P e. _V
6 hash1snb
 |-  ( P e. _V -> ( ( # ` P ) = 1 <-> E. x P = { x } ) )
7 5 6 ax-mp
 |-  ( ( # ` P ) = 1 <-> E. x P = { x } )
8 2 7 sylib
 |-  ( ph -> E. x P = { x } )
9 3 adantr
 |-  ( ( ph /\ P = { x } ) -> A e. P )
10 simpr
 |-  ( ( ph /\ P = { x } ) -> P = { x } )
11 9 10 eleqtrd
 |-  ( ( ph /\ P = { x } ) -> A e. { x } )
12 elsni
 |-  ( A e. { x } -> A = x )
13 11 12 syl
 |-  ( ( ph /\ P = { x } ) -> A = x )
14 4 adantr
 |-  ( ( ph /\ P = { x } ) -> B e. P )
15 14 10 eleqtrd
 |-  ( ( ph /\ P = { x } ) -> B e. { x } )
16 elsni
 |-  ( B e. { x } -> B = x )
17 15 16 syl
 |-  ( ( ph /\ P = { x } ) -> B = x )
18 13 17 eqtr4d
 |-  ( ( ph /\ P = { x } ) -> A = B )
19 8 18 exlimddv
 |-  ( ph -> A = B )