Metamath Proof Explorer

Theorem axpre-lttrn

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

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

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 elreal 
 |-  ( C e. RR <-> E. z e. R. <. z , 0R >. = C )
4 breq1 
 |-  ( <. x , 0R >. = A -> ( <. x , 0R >. . <-> A . ) )
5 4 anbi1d 
 |-  ( <. x , 0R >. = A -> ( ( <. x , 0R >. . /\ <. y , 0R >. . ) <-> ( A . /\ <. y , 0R >. . ) ) )
6 breq1 
 |-  ( <. x , 0R >. = A -> ( <. x , 0R >. . <-> A . ) )
7 5 6 imbi12d 
 |-  ( <. x , 0R >. = A -> ( ( ( <. x , 0R >. . /\ <. y , 0R >. . ) -> <. x , 0R >. . ) <-> ( ( A . /\ <. y , 0R >. . ) -> A . ) ) )
8 breq2 
 |-  ( <. y , 0R >. = B -> ( A . <-> A
9 breq1 
 |-  ( <. y , 0R >. = B -> ( <. y , 0R >. . <-> B . ) )
10 8 9 anbi12d 
 |-  ( <. y , 0R >. = B -> ( ( A . /\ <. y , 0R >. . ) <-> ( A . ) ) )
11 10 imbi1d 
 |-  ( <. y , 0R >. = B -> ( ( ( A . /\ <. y , 0R >. . ) -> A . ) <-> ( ( A . ) -> A . ) ) )
12 breq2 
 |-  ( <. z , 0R >. = C -> ( B . <-> B
13 12 anbi2d 
 |-  ( <. z , 0R >. = C -> ( ( A . ) <-> ( A
14 breq2 
 |-  ( <. z , 0R >. = C -> ( A . <-> A
15 13 14 imbi12d 
 |-  ( <. z , 0R >. = C -> ( ( ( A . ) -> A . ) <-> ( ( A  A
16 ltresr 
 |-  ( <. x , 0R >. . <-> x
17 ltresr 
 |-  ( <. y , 0R >. . <-> y
18 ltsosr 
 |-
19 ltrelsr 
 |-
20 18 19 sotri 
 |-  ( ( x  x
21 16 17 20 syl2anb 
 |-  ( ( <. x , 0R >. . /\ <. y , 0R >. . ) -> x
22 ltresr 
 |-  ( <. x , 0R >. . <-> x
23 21 22 sylibr 
 |-  ( ( <. x , 0R >. . /\ <. y , 0R >. . ) -> <. x , 0R >. . )
24 23 a1i 
 |-  ( ( x e. R. /\ y e. R. /\ z e. R. ) -> ( ( <. x , 0R >. . /\ <. y , 0R >. . ) -> <. x , 0R >. . ) )
25 1 2 3 7 11 15 24 3gencl 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A  A