Metamath Proof Explorer

Theorem qextle

Description: An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion qextle 
|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> A. x e. QQ ( x <_ A <-> x <_ B ) ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( A = B -> ( x <_ A <-> x <_ B ) )
2 1 ralrimivw 
 |-  ( A = B -> A. x e. QQ ( x <_ A <-> x <_ B ) )
3 xrlttri2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A =/= B <-> ( A < B \/ B < A ) ) )
4 qextltlem 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. QQ ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) ) )
5 simpr 
 |-  ( ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) -> -. ( x <_ A <-> x <_ B ) )
6 5 reximi 
 |-  ( E. x e. QQ ( -. ( x < A <-> x < B ) /\ -. ( x <_ A <-> x <_ B ) ) -> E. x e. QQ -. ( x <_ A <-> x <_ B ) )
7 4 6 syl6 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. QQ -. ( x <_ A <-> x <_ B ) ) )
8 qextltlem 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B < A -> E. x e. QQ ( -. ( x < B <-> x < A ) /\ -. ( x <_ B <-> x <_ A ) ) ) )
9 simpr 
 |-  ( ( -. ( x < B <-> x < A ) /\ -. ( x <_ B <-> x <_ A ) ) -> -. ( x <_ B <-> x <_ A ) )
10 bicom 
 |-  ( ( x <_ B <-> x <_ A ) <-> ( x <_ A <-> x <_ B ) )
11 9 10 sylnib 
 |-  ( ( -. ( x < B <-> x < A ) /\ -. ( x <_ B <-> x <_ A ) ) -> -. ( x <_ A <-> x <_ B ) )
12 11 reximi 
 |-  ( E. x e. QQ ( -. ( x < B <-> x < A ) /\ -. ( x <_ B <-> x <_ A ) ) -> E. x e. QQ -. ( x <_ A <-> x <_ B ) )
13 8 12 syl6 
 |-  ( ( B e. RR* /\ A e. RR* ) -> ( B < A -> E. x e. QQ -. ( x <_ A <-> x <_ B ) ) )
14 13 ancoms 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B < A -> E. x e. QQ -. ( x <_ A <-> x <_ B ) ) )
15 7 14 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A < B \/ B < A ) -> E. x e. QQ -. ( x <_ A <-> x <_ B ) ) )
16 3 15 sylbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A =/= B -> E. x e. QQ -. ( x <_ A <-> x <_ B ) ) )
17 rexnal 
 |-  ( E. x e. QQ -. ( x <_ A <-> x <_ B ) <-> -. A. x e. QQ ( x <_ A <-> x <_ B ) )
18 16 17 syl6ib 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A =/= B -> -. A. x e. QQ ( x <_ A <-> x <_ B ) ) )
19 18 necon4ad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A. x e. QQ ( x <_ A <-> x <_ B ) -> A = B ) )
20 2 19 impbid2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> A. x e. QQ ( x <_ A <-> x <_ B ) ) )