Metamath Proof Explorer

Definition df-itv

Description: Define the Interval (segment) index extractor for Tarski geometries. (Contributed by Thierry Arnoux, 24-Aug-2017)

Ref Expression
Assertion df-itv 
|- Itv = Slot ; 1 6

Detailed syntax breakdown

Step Hyp Ref Expression
0 citv 
 |-  Itv
1 c1 
 |-  1
2 c6 
 |-  6
3 1 2 cdc 
 |-  ; 1 6
4 3 cslot 
 |-  Slot ; 1 6
5 0 4 wceq 
 |-  Itv = Slot ; 1 6