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