This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem solin

Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996)

Ref Expression
Assertion solin 
|- ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = B -> ( x R y <-> B R y ) )
2 eqeq1 
 |-  ( x = B -> ( x = y <-> B = y ) )
3 breq2 
 |-  ( x = B -> ( y R x <-> y R B ) )
4 1 2 3 3orbi123d 
 |-  ( x = B -> ( ( x R y \/ x = y \/ y R x ) <-> ( B R y \/ B = y \/ y R B ) ) )
5 4 imbi2d 
 |-  ( x = B -> ( ( R Or A -> ( x R y \/ x = y \/ y R x ) ) <-> ( R Or A -> ( B R y \/ B = y \/ y R B ) ) ) )
6 breq2 
 |-  ( y = C -> ( B R y <-> B R C ) )
7 eqeq2 
 |-  ( y = C -> ( B = y <-> B = C ) )
8 breq1 
 |-  ( y = C -> ( y R B <-> C R B ) )
9 6 7 8 3orbi123d 
 |-  ( y = C -> ( ( B R y \/ B = y \/ y R B ) <-> ( B R C \/ B = C \/ C R B ) ) )
10 9 imbi2d 
 |-  ( y = C -> ( ( R Or A -> ( B R y \/ B = y \/ y R B ) ) <-> ( R Or A -> ( B R C \/ B = C \/ C R B ) ) ) )
11 df-so 
 |-  ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
12 breq1 
 |-  ( x = z -> ( x R y <-> z R y ) )
13 equequ1 
 |-  ( x = z -> ( x = y <-> z = y ) )
14 breq2 
 |-  ( x = z -> ( y R x <-> y R z ) )
15 12 13 14 3orbi123d 
 |-  ( x = z -> ( ( x R y \/ x = y \/ y R x ) <-> ( z R y \/ z = y \/ y R z ) ) )
16 15 ralbidv 
 |-  ( x = z -> ( A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A ( z R y \/ z = y \/ y R z ) ) )
17 16 rspw 
 |-  ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> ( x e. A -> A. y e. A ( x R y \/ x = y \/ y R x ) ) )
18 breq2 
 |-  ( y = z -> ( x R y <-> x R z ) )
19 equequ2 
 |-  ( y = z -> ( x = y <-> x = z ) )
20 breq1 
 |-  ( y = z -> ( y R x <-> z R x ) )
21 18 19 20 3orbi123d 
 |-  ( y = z -> ( ( x R y \/ x = y \/ y R x ) <-> ( x R z \/ x = z \/ z R x ) ) )
22 21 rspw 
 |-  ( A. y e. A ( x R y \/ x = y \/ y R x ) -> ( y e. A -> ( x R y \/ x = y \/ y R x ) ) )
23 17 22 syl6 
 |-  ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> ( x e. A -> ( y e. A -> ( x R y \/ x = y \/ y R x ) ) ) )
24 23 impd 
 |-  ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
25 11 24 simplbiim 
 |-  ( R Or A -> ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
26 25 com12 
 |-  ( ( x e. A /\ y e. A ) -> ( R Or A -> ( x R y \/ x = y \/ y R x ) ) )
27 5 10 26 vtocl2ga 
 |-  ( ( B e. A /\ C e. A ) -> ( R Or A -> ( B R C \/ B = C \/ C R B ) ) )
28 27 impcom 
 |-  ( ( R Or A /\ ( B e. A /\ C e. A ) ) -> ( B R C \/ B = C \/ C R B ) )