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	syl6bb	|- ( ( <. 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