Metamath Proof Explorer


Theorem axpre-lttri

Description: Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttri . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion axpre-lttri
|- ( ( A e. RR /\ B e. RR ) -> ( A  -. ( A = B \/ B 

Proof

Step Hyp Ref Expression
1 elreal
 |-  ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
2 elreal
 |-  ( B e. RR <-> E. y e. R. <. y , 0R >. = B )
3 breq1
 |-  ( <. x , 0R >. = A -> ( <. x , 0R >. . <-> A . ) )
4 eqeq1
 |-  ( <. x , 0R >. = A -> ( <. x , 0R >. = <. y , 0R >. <-> A = <. y , 0R >. ) )
5 breq2
 |-  ( <. x , 0R >. = A -> ( <. y , 0R >. . <-> <. y , 0R >. 
6 4 5 orbi12d
 |-  ( <. x , 0R >. = A -> ( ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> ( A = <. y , 0R >. \/ <. y , 0R >. 
7 6 notbid
 |-  ( <. x , 0R >. = A -> ( -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> -. ( A = <. y , 0R >. \/ <. y , 0R >. 
8 3 7 bibi12d
 |-  ( <. x , 0R >. = A -> ( ( <. x , 0R >. . <-> -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) ) <-> ( A . <-> -. ( A = <. y , 0R >. \/ <. y , 0R >. 
9 breq2
 |-  ( <. y , 0R >. = B -> ( A . <-> A 
10 eqeq2
 |-  ( <. y , 0R >. = B -> ( A = <. y , 0R >. <-> A = B ) )
11 breq1
 |-  ( <. y , 0R >. = B -> ( <. y , 0R >.  B 
12 10 11 orbi12d
 |-  ( <. y , 0R >. = B -> ( ( A = <. y , 0R >. \/ <. y , 0R >.  ( A = B \/ B 
13 12 notbid
 |-  ( <. y , 0R >. = B -> ( -. ( A = <. y , 0R >. \/ <. y , 0R >.  -. ( A = B \/ B 
14 9 13 bibi12d
 |-  ( <. y , 0R >. = B -> ( ( A . <-> -. ( A = <. y , 0R >. \/ <. y , 0R >.  ( A  -. ( A = B \/ B 
15 ltsosr
 |-  
16 sotric
 |-  ( (  ( x  -. ( x = y \/ y 
17 15 16 mpan
 |-  ( ( x e. R. /\ y e. R. ) -> ( x  -. ( x = y \/ y 
18 ltresr
 |-  ( <. x , 0R >. . <-> x 
19 vex
 |-  x e. _V
20 19 eqresr
 |-  ( <. x , 0R >. = <. y , 0R >. <-> x = y )
21 ltresr
 |-  ( <. y , 0R >. . <-> y 
22 20 21 orbi12i
 |-  ( ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> ( x = y \/ y 
23 22 notbii
 |-  ( -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) <-> -. ( x = y \/ y 
24 17 18 23 3bitr4g
 |-  ( ( x e. R. /\ y e. R. ) -> ( <. x , 0R >. . <-> -. ( <. x , 0R >. = <. y , 0R >. \/ <. y , 0R >. . ) ) )
25 1 2 8 14 24 2gencl
 |-  ( ( A e. RR /\ B e. RR ) -> ( A  -. ( A = B \/ B