Metamath Proof Explorer


Theorem tsrlin

Description: A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypothesis istsr.1 X=domR
Assertion tsrlin RTosetRelAXBXARBBRA

Proof

Step Hyp Ref Expression
1 istsr.1 X=domR
2 1 istsr2 RTosetRelRPosetRelxXyXxRyyRx
3 2 simprbi RTosetRelxXyXxRyyRx
4 breq1 x=AxRyARy
5 breq2 x=AyRxyRA
6 4 5 orbi12d x=AxRyyRxARyyRA
7 breq2 y=BARyARB
8 breq1 y=ByRABRA
9 7 8 orbi12d y=BARyyRAARBBRA
10 6 9 rspc2v AXBXxXyXxRyyRxARBBRA
11 3 10 syl5com RTosetRelAXBXARBBRA
12 11 3impib RTosetRelAXBXARBBRA