Theorem tgldim0itv

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

	Ref	Expression
Hypotheses	tgbtwndiff.p	|- P = ( Base ` G )
	tgbtwndiff.d	|- .- = ( dist ` G )
	tgbtwndiff.i	|- I = ( Itv ` G )
	tgbtwndiff.g	|- ( ph -> G e. TarskiG )
	tgbtwndiff.a	|- ( ph -> A e. P )
	tgbtwndiff.b	|- ( ph -> B e. P )
	tgldim0itv.c	|- ( ph -> C e. P )
	tgldim0itv.p	|- ( ph -> ( # ` P ) = 1 )
Assertion	tgldim0itv	|- ( ph -> A e. ( B I C ) )

Proof

Step	Hyp	Ref	Expression
1		tgbtwndiff.p	|- P = ( Base ` G )
2		tgbtwndiff.d	|- .- = ( dist ` G )
3		tgbtwndiff.i	|- I = ( Itv ` G )
4		tgbtwndiff.g	|- ( ph -> G e. TarskiG )
5		tgbtwndiff.a	|- ( ph -> A e. P )
6		tgbtwndiff.b	|- ( ph -> B e. P )
7		tgldim0itv.c	|- ( ph -> C e. P )
8		tgldim0itv.p	|- ( ph -> ( # ` P ) = 1 )
9	1 8 5 6	tgldim0eq	|- ( ph -> A = B )
10	1 2 3 4 6 7	tgbtwntriv1	|- ( ph -> B e. ( B I C ) )
11	9 10	eqeltrd	|- ( ph -> A e. ( B I C ) )