Theorem trkgitv

Description: The congruence relation in 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	trkgitv	|- ( I e. V -> I = ( Itv ` 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		itvid	|- Itv = Slot ( Itv ` ndx )
4		snsstp3	|- { <. ( Itv ` ndx ) , I >. } C_ { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
5	4 1	sseqtrri	|- { <. ( Itv ` ndx ) , I >. } C_ W
6	2 3 5	strfv	|- ( I e. V -> I = ( Itv ` W ) )