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	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgbas.1	⊢ 𝐵 = ( Base ‘ 𝐻 )
Assertion	ttgbas	⊢ 𝐵 = ( Base ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgbas.1	⊢ 𝐵 = ( Base ‘ 𝐻 )
3		df-base	⊢ Base = Slot 1
4		1nn	⊢ 1 ∈ ℕ
5		6nn0	⊢ 6 ∈ ℕ0
6		1nn0	⊢ 1 ∈ ℕ0
7		1lt10	⊢ 1 < ; 1 0
8	4 5 6 7	declti	⊢ 1 < ; 1 6
9	1 3 4 8	ttglem	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐺 )
10	2 9	eqtri	⊢ 𝐵 = ( Base ‘ 𝐺 )