Theorem ttgbas

Description: The base set of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019)

	Ref	Expression
Hypotheses	ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
	ttgbas.1	$$⊢B={\mathrm{Base}}_H$$
Assertion	ttgbas	$$⊢B={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgbas.1	$$⊢B={\mathrm{Base}}_H$$
3		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
4		1nn	$$⊢1\in \mathbb{N}$$
5		6nn0	$$⊢6\in {\mathbb{N}}_0$$
6		1nn0	$$⊢1\in {\mathbb{N}}_0$$
7		1lt10	$$⊢1<10$$
8	4 5 6 7	declti	$$⊢1<16$$
9	1 3 4 8	ttglem	$$⊢{\mathrm{Base}}_H={\mathrm{Base}}_G$$
10	2 9	eqtri	$$⊢B={\mathrm{Base}}_G$$