Theorem tgldim0itv

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

	Ref	Expression
Hypotheses	tgbtwndiff.p	$$⊢P={\mathrm{Base}}_G$$
	tgbtwndiff.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	tgbtwndiff.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	tgbtwndiff.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	tgbtwndiff.a	$$⊢\phi \to A\in P$$
	tgbtwndiff.b	$$⊢\phi \to B\in P$$
	tgldim0itv.c	$$⊢\phi \to C\in P$$
	tgldim0itv.p	$$⊢\phi \to \left|P\right|=1$$
Assertion	tgldim0itv	$$⊢\phi \to A\in \left(BIC\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgbtwndiff.p	$$⊢P={\mathrm{Base}}_G$$
2		tgbtwndiff.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		tgbtwndiff.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		tgbtwndiff.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		tgbtwndiff.a	$$⊢\phi \to A\in P$$
6		tgbtwndiff.b	$$⊢\phi \to B\in P$$
7		tgldim0itv.c	$$⊢\phi \to C\in P$$
8		tgldim0itv.p	$$⊢\phi \to \left|P\right|=1$$
9	1 8 5 6	tgldim0eq	$$⊢\phi \to A=B$$
10	1 2 3 4 6 7	tgbtwntriv1	$$⊢\phi \to B\in \left(BIC\right)$$
11	9 10	eqeltrd	$$⊢\phi \to A\in \left(BIC\right)$$