Metamath Proof Explorer


Theorem qextlt

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

Ref Expression
Assertion qextlt
|- ( ( 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 simpl
 |-  ( ( -. ( 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 simpl
 |-  ( ( -. ( 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 ) ) )