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 = dom R
Assertion tsrlin 
|- ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B \/ B R A ) )

Proof

Step Hyp Ref Expression
1 istsr.1 
 |-  X = dom R
2 1 istsr2 
 |-  ( R e. TosetRel <-> ( R e. PosetRel /\ A. x e. X A. y e. X ( x R y \/ y R x ) ) )
3 2 simprbi 
 |-  ( R e. TosetRel -> A. x e. X A. y e. X ( x R y \/ y R x ) )
4 breq1 
 |-  ( x = A -> ( x R y <-> A R y ) )
5 breq2 
 |-  ( x = A -> ( y R x <-> y R A ) )
6 4 5 orbi12d 
 |-  ( x = A -> ( ( x R y \/ y R x ) <-> ( A R y \/ y R A ) ) )
7 breq2 
 |-  ( y = B -> ( A R y <-> A R B ) )
8 breq1 
 |-  ( y = B -> ( y R A <-> B R A ) )
9 7 8 orbi12d 
 |-  ( y = B -> ( ( A R y \/ y R A ) <-> ( A R B \/ B R A ) ) )
10 6 9 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( x R y \/ y R x ) -> ( A R B \/ B R A ) ) )
11 3 10 syl5com 
 |-  ( R e. TosetRel -> ( ( A e. X /\ B e. X ) -> ( A R B \/ B R A ) ) )
12 11 3impib 
 |-  ( ( R e. TosetRel /\ A e. X /\ B e. X ) -> ( A R B \/ B R A ) )