Theorem trkgbas

Description: The base set of a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017)

	Ref	Expression
Hypothesis	trkgstr.w	|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
Assertion	trkgbas	|- ( U e. V -> U = ( Base ` W ) )

Proof

Step	Hyp	Ref	Expression
1		trkgstr.w	|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
2	1	trkgstr	|- W Struct <. 1 , ; 1 6 >.
3		baseid	|- Base = Slot ( Base ` ndx )
4		snsstp1	|- { <. ( Base ` ndx ) , U >. } C_ { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
5	4 1	sseqtrri	|- { <. ( Base ` ndx ) , U >. } C_ W
6	2 3 5	strfv	|- ( U e. V -> U = ( Base ` W ) )