Metamath Proof Explorer


Theorem ltresr

Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltresr
|- ( <. A , 0R >. . <-> A 

Proof

Step Hyp Ref Expression
1 ltrelre
 |-  
2 1 brel
 |-  ( <. A , 0R >. . -> ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) )
3 opelreal
 |-  ( <. A , 0R >. e. RR <-> A e. R. )
4 opelreal
 |-  ( <. B , 0R >. e. RR <-> B e. R. )
5 3 4 anbi12i
 |-  ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) <-> ( A e. R. /\ B e. R. ) )
6 2 5 sylib
 |-  ( <. A , 0R >. . -> ( A e. R. /\ B e. R. ) )
7 ltrelsr
 |-  
8 7 brel
 |-  ( A  ( A e. R. /\ B e. R. ) )
9 opex
 |-  <. A , 0R >. e. _V
10 opex
 |-  <. B , 0R >. e. _V
11 eleq1
 |-  ( x = <. A , 0R >. -> ( x e. RR <-> <. A , 0R >. e. RR ) )
12 11 anbi1d
 |-  ( x = <. A , 0R >. -> ( ( x e. RR /\ y e. RR ) <-> ( <. A , 0R >. e. RR /\ y e. RR ) ) )
13 eqeq1
 |-  ( x = <. A , 0R >. -> ( x = <. z , 0R >. <-> <. A , 0R >. = <. z , 0R >. ) )
14 13 anbi1d
 |-  ( x = <. A , 0R >. -> ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) <-> ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) ) )
15 14 anbi1d
 |-  ( x = <. A , 0R >. -> ( ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z  ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
16 15 2exbidv
 |-  ( x = <. A , 0R >. -> ( E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z  E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
17 12 16 anbi12d
 |-  ( x = <. A , 0R >. -> ( ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z  ( ( <. A , 0R >. e. RR /\ y e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
18 eleq1
 |-  ( y = <. B , 0R >. -> ( y e. RR <-> <. B , 0R >. e. RR ) )
19 18 anbi2d
 |-  ( y = <. B , 0R >. -> ( ( <. A , 0R >. e. RR /\ y e. RR ) <-> ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) ) )
20 eqeq1
 |-  ( y = <. B , 0R >. -> ( y = <. w , 0R >. <-> <. B , 0R >. = <. w , 0R >. ) )
21 20 anbi2d
 |-  ( y = <. B , 0R >. -> ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) <-> ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) ) )
22 21 anbi1d
 |-  ( y = <. B , 0R >. -> ( ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z  ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z 
23 22 2exbidv
 |-  ( y = <. B , 0R >. -> ( E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z  E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z 
24 19 23 anbi12d
 |-  ( y = <. B , 0R >. -> ( ( ( <. A , 0R >. e. RR /\ y e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z  ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z 
25 df-lt
 |-  . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z 
26 9 10 17 24 25 brab
 |-  ( <. A , 0R >. . <-> ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) /\ E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z 
27 26 baib
 |-  ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) -> ( <. A , 0R >. . <-> E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z 
28 vex
 |-  z e. _V
29 28 eqresr
 |-  ( <. z , 0R >. = <. A , 0R >. <-> z = A )
30 eqcom
 |-  ( <. A , 0R >. = <. z , 0R >. <-> <. z , 0R >. = <. A , 0R >. )
31 eqcom
 |-  ( A = z <-> z = A )
32 29 30 31 3bitr4i
 |-  ( <. A , 0R >. = <. z , 0R >. <-> A = z )
33 vex
 |-  w e. _V
34 33 eqresr
 |-  ( <. w , 0R >. = <. B , 0R >. <-> w = B )
35 eqcom
 |-  ( <. B , 0R >. = <. w , 0R >. <-> <. w , 0R >. = <. B , 0R >. )
36 eqcom
 |-  ( B = w <-> w = B )
37 34 35 36 3bitr4i
 |-  ( <. B , 0R >. = <. w , 0R >. <-> B = w )
38 32 37 anbi12i
 |-  ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) <-> ( A = z /\ B = w ) )
39 28 33 opth2
 |-  ( <. A , B >. = <. z , w >. <-> ( A = z /\ B = w ) )
40 38 39 bitr4i
 |-  ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) <-> <. A , B >. = <. z , w >. )
41 40 anbi1i
 |-  ( ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z  ( <. A , B >. = <. z , w >. /\ z 
42 41 2exbii
 |-  ( E. z E. w ( ( <. A , 0R >. = <. z , 0R >. /\ <. B , 0R >. = <. w , 0R >. ) /\ z  E. z E. w ( <. A , B >. = <. z , w >. /\ z 
43 27 42 bitrdi
 |-  ( ( <. A , 0R >. e. RR /\ <. B , 0R >. e. RR ) -> ( <. A , 0R >. . <-> E. z E. w ( <. A , B >. = <. z , w >. /\ z 
44 3 4 43 syl2anbr
 |-  ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. . <-> E. z E. w ( <. A , B >. = <. z , w >. /\ z 
45 breq12
 |-  ( ( z = A /\ w = B ) -> ( z  A 
46 45 copsex2g
 |-  ( ( A e. R. /\ B e. R. ) -> ( E. z E. w ( <. A , B >. = <. z , w >. /\ z  A 
47 44 46 bitrd
 |-  ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. . <-> A 
48 6 8 47 pm5.21nii
 |-  ( <. A , 0R >. . <-> A