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 )