This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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