Theorem ltresr 4052

Description: Ordering of real subset of complex numbers in terms of signed reals.

Hypotheses

Ref	Expression
ltresr.1	|- A e. V
ltresr.2	|- B e. V

Assertion

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

Proof of Theorem ltresr

Step	Hyp	Ref	Expression
1		opex 1893	. . . 4 |- <.B, 0R>. e. V
2		ltrelre 4046	. . . 4 |- < (_ (RR X. RR)
3	1, 2	brel 2459	. . 3 |- (<.A, 0R>. < <.B, 0R>. -> (<.A, 0R>. e. RR /\ <.B, 0R>. e. RR))
4		opelreal 4043	. . . 4 |- (<.A, 0R>. e. RR <-> A e. R.)
5		opelreal 4043	. . . 4 |- (<.B, 0R>. e. RR <-> B e. R.)
6	4, 5	anbi12i 369	. . 3 |- ((<.A, 0R>. e. RR /\ <.B, 0R>. e. RR) <-> (A e. R. /\ B e. R.))
7	3, 6	sylib 173	. 2 |- (<.A, 0R>. < <.B, 0R>. -> (A e. R. /\ B e. R.))
8		ltresr.2	. . 3 |- B e. V
9		ltrelsr 3974	. . 3 |- <R (_ (R. X. R.)
10	8, 9	brel 2459	. 2 |- (A <R B -> (A e. R. /\ B e. R.))
11		opex 1893	. . . . . . 7 |- <.A, 0R>. e. V
12		eleq1 1149	. . . . . . . . 9 |- (x = <.A, 0R>. -> (x e. RR <-> <.A, 0R>. e. RR))
13	12	anbi1d 469	. . . . . . . 8 |- (x = <.A, 0R>. -> ((x e. RR /\ y e. RR) <-> (<.A, 0R>. e. RR /\ y e. RR)))
14		cleq1 1107	. . . . . . . . . . 11 |- (x = <.A, 0R>. -> (x = <.z, 0R>. <-> <.A, 0R>. = <.z, 0R>.))
15	14	anbi1d 469	. . . . . . . . . 10 |- (x = <.A, 0R>. -> ((x = <.z, 0R>. /\ y = <.w, 0R>.) <-> (<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.)))
16	15	anbi1d 469	. . . . . . . . 9 |- (x = <.A, 0R>. -> (((x = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w) <-> ((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w)))
17	16	bi2exdv 938	. . . . . . . 8 |- (x = <.A, 0R>. -> (E.zE.w((x = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w) <-> E.zE.w((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w)))
18	13, 17	anbi12d 476	. . . . . . 7 |- (x = <.A, 0R>. -> (((x e. RR /\ y e. RR) /\ E.zE.w((x = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w)) <-> ((<.A, 0R>. e. RR /\ y e. RR) /\ E.zE.w((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w))))
19		eleq1 1149	. . . . . . . . 9 |- (y = <.B, 0R>. -> (y e. RR <-> <.B, 0R>. e. RR))
20	19	anbi2d 468	. . . . . . . 8 |- (y = <.B, 0R>. -> ((<.A, 0R>. e. RR /\ y e. RR) <-> (<.A, 0R>. e. RR /\ <.B, 0R>. e. RR)))
21		cleq1 1107	. . . . . . . . . . 11 |- (y = <.B, 0R>. -> (y = <.w, 0R>. <-> <.B, 0R>. = <.w, 0R>.))
22	21	anbi2d 468	. . . . . . . . . 10 |- (y = <.B, 0R>. -> ((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) <-> (<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.)))
23	22	anbi1d 469	. . . . . . . . 9 |- (y = <.B, 0R>. -> (((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w) <-> ((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w)))
24	23	bi2exdv 938	. . . . . . . 8 |- (y = <.B, 0R>. -> (E.zE.w((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w) <-> E.zE.w((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w)))
25	20, 24	anbi12d 476	. . . . . . 7 |- (y = <.B, 0R>. -> (((<.A, 0R>. e. RR /\ y e. RR) /\ E.zE.w((<.A, 0R>. = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w)) <-> ((<.A, 0R>. e. RR /\ <.B, 0R>. e. RR) /\ E.zE.w((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w))))
26		df-lt 4041	. . . . . . 7 |- < = {<.x, y>. | ((x e. RR /\ y e. RR) /\ E.zE.w((x = <.z, 0R>. /\ y = <.w, 0R>.) /\ z <R w))}
27	11, 1, 18, 25, 26	brab 2118	. . . . . 6 |- (<.A, 0R>. < <.B, 0R>. <-> ((<.A, 0R>. e. RR /\ <.B, 0R>. e. RR) /\ E.zE.w((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w)))
28	27	baib 506	. . . . 5 |- ((<.A, 0R>. e. RR /\ <.B, 0R>. e. RR) -> (<.A, 0R>. < <.B, 0R>. <-> E.zE.w((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w)))
29		ltresr.1	. . . . . . . . . 10 |- A e. V
30	29	eqresr 4049	. . . . . . . . 9 |- (<.A, 0R>. = <.z, 0R>. <-> A = z)
31	8	eqresr 4049	. . . . . . . . 9 |- (<.B, 0R>. = <.w, 0R>. <-> B = w)
32	30, 31	anbi12i 369	. . . . . . . 8 |- ((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) <-> (A = z /\ B = w))
33		visset 1350	. . . . . . . . 9 |- w e. V
34	29, 8, 33	opth 1898	. . . . . . . 8 |- (<.A, B>. = <.z, w>. <-> (A = z /\ B = w))
35	32, 34	bitr4 154	. . . . . . 7 |- ((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) <-> <.A, B>. = <.z, w>.)
36	35	anbi1i 368	. . . . . 6 |- (((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w) <-> (<.A, B>. = <.z, w>. /\ z <R w))
37	36	bi2ex 734	. . . . 5 |- (E.zE.w((<.A, 0R>. = <.z, 0R>. /\ <.B, 0R>. = <.w, 0R>.) /\ z <R w) <-> E.zE.w(<.A, B>. = <.z, w>. /\ z <R w))
38	28, 37	syl6bb 414	. . . 4 |- ((<.A, 0R>. e. RR /\ <.B, 0R>. e. RR) -> (<.A, 0R>. < <.B, 0R>. <-> E.zE.w(<.A, B>. = <.z, w>. /\ z <R w)))
39	38, 4, 5	syl2anbr 351	. . 3 |- ((A e. R. /\ B e. R.) -> (<.A, 0R>. < <.B, 0R>. <-> E.zE.w(<.A, B>. = <.z, w>. /\ z <R w)))
40		breq12 2067	. . . 4 |- ((z = A /\ w = B) -> (z <R w <-> A <R B))
41	40	copsex2g 1903	. . 3 |- ((A e. R. /\ B e. R.) -> (E.zE.w(<.A, B>. = <.z, w>. /\ z <R w) <-> A <R B))
42	39, 41	bitrd 406	. 2 |- ((A e. R. /\ B e. R.) -> (<.A, 0R>. < <.B, 0R>. <-> A <R B))
43	7, 10, 42	pm5.21nii 504	1 |- (<.A, 0R>. < <.B, 0R>. <-> A <R B)

Syntax hints:   <-> wb 127   /\ wa 196  E.wex 678   = wceq 1091   e. wcel 1092  Vcvv 1348  <.cop 1810   class class class wbr 2054  R.cnr 3787  0Rc0r 3788   <R cltr 3793  RRcr 4027   < clt 4033

This theorem is referenced by:  supre 4054  ltsor 4055  axltadd 4085  axmulgt0 4086

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-1p 3881  df-enr 3960  df-nr 3961  df-ltr 3964  df-0r 3965  df-r 4038  df-lt 4041

metamath.org