Theorem ltresr 7934

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

Assertion

Ref	Expression
ltresr	⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)

Proof of Theorem ltresr

Dummy variables 𝑥 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelre 7928	. . . 4 ⊢ <ℝ ⊆ (ℝ × ℝ)
2	1	brel 4725	. . 3 ⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ → (⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ))
3		opelreal 7922	. . . 4 ⊢ (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴 ∈ R)
4		opelreal 7922	. . . 4 ⊢ (⟨𝐵, 0R⟩ ∈ ℝ ↔ 𝐵 ∈ R)
5	3, 4	anbi12i 460	. . 3 ⊢ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) ↔ (𝐴 ∈ R ∧ 𝐵 ∈ R))
6	2, 5	sylib 122	. 2 ⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ → (𝐴 ∈ R ∧ 𝐵 ∈ R))
7		ltrelsr 7833	. . 3 ⊢ <R ⊆ (R × R)
8	7	brel 4725	. 2 ⊢ (𝐴 <R 𝐵 → (𝐴 ∈ R ∧ 𝐵 ∈ R))
9		eleq1 2267	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → (𝑥 ∈ ℝ ↔ ⟨𝐴, 0R⟩ ∈ ℝ))
10	9	anbi1d 465	. . . . . . . 8 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ)))
11		eqeq1 2211	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → (𝑥 = ⟨𝑧, 0R⟩ ↔ ⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩))
12	11	anbi1d 465	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → ((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ↔ (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩)))
13	12	anbi1d 465	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → (((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
14	13	2exbidv 1890	. . . . . . . 8 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → (∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
15	10, 14	anbi12d 473	. . . . . . 7 ⊢ (𝑥 = ⟨𝐴, 0R⟩ → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)) ↔ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))))
16		eleq1 2267	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → (𝑦 ∈ ℝ ↔ ⟨𝐵, 0R⟩ ∈ ℝ))
17	16	anbi2d 464	. . . . . . . 8 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → ((⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ)))
18		eqeq1 2211	. . . . . . . . . . 11 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → (𝑦 = ⟨𝑤, 0R⟩ ↔ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩))
19	18	anbi2d 464	. . . . . . . . . 10 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ↔ (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩)))
20	19	anbi1d 465	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → (((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
21	20	2exbidv 1890	. . . . . . . 8 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → (∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
22	17, 21	anbi12d 473	. . . . . . 7 ⊢ (𝑦 = ⟨𝐵, 0R⟩ → (((⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)) ↔ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))))
23		df-lt 7920	. . . . . . 7 ⊢ <ℝ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧∃𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
24	15, 22, 23	brabg 4313	. . . . . 6 ⊢ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) → (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) ∧ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))))
25	24	bianabs 611	. . . . 5 ⊢ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) → (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ ∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
26		vex 2774	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
27	26	eqresr 7931	. . . . . . . . . 10 ⊢ (⟨𝑧, 0R⟩ = ⟨𝐴, 0R⟩ ↔ 𝑧 = 𝐴)
28		eqcom 2206	. . . . . . . . . 10 ⊢ (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ↔ ⟨𝑧, 0R⟩ = ⟨𝐴, 0R⟩)
29		eqcom 2206	. . . . . . . . . 10 ⊢ (𝐴 = 𝑧 ↔ 𝑧 = 𝐴)
30	27, 28, 29	3bitr4i 212	. . . . . . . . 9 ⊢ (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ↔ 𝐴 = 𝑧)
31		vex 2774	. . . . . . . . . . 11 ⊢ 𝑤 ∈ V
32	31	eqresr 7931	. . . . . . . . . 10 ⊢ (⟨𝑤, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝑤 = 𝐵)
33		eqcom 2206	. . . . . . . . . 10 ⊢ (⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩ ↔ ⟨𝑤, 0R⟩ = ⟨𝐵, 0R⟩)
34		eqcom 2206	. . . . . . . . . 10 ⊢ (𝐵 = 𝑤 ↔ 𝑤 = 𝐵)
35	32, 33, 34	3bitr4i 212	. . . . . . . . 9 ⊢ (⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩ ↔ 𝐵 = 𝑤)
36	30, 35	anbi12i 460	. . . . . . . 8 ⊢ ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝑤))
37	26, 31	opth2 4283	. . . . . . . 8 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ↔ (𝐴 = 𝑧 ∧ 𝐵 = 𝑤))
38	36, 37	bitr4i 187	. . . . . . 7 ⊢ ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩)
39	38	anbi1i 458	. . . . . 6 ⊢ (((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))
40	39	2exbii 1628	. . . . 5 ⊢ (∃𝑧∃𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))
41	25, 40	bitrdi 196	. . . 4 ⊢ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) → (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)))
42	3, 4, 41	syl2anbr 292	. . 3 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ ∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)))
43		breq12 4048	. . . 4 ⊢ ((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → (𝑧 <R 𝑤 ↔ 𝐴 <R 𝐵))
44	43	copsex2g 4289	. . 3 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (∃𝑧∃𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤) ↔ 𝐴 <R 𝐵))
45	42, 44	bitrd 188	. 2 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵))
46	6, 8, 45	pm5.21nii 705	1 ⊢ (⟨𝐴, 0R⟩ <ℝ ⟨𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1372  ∃wex 1514   ∈ wcel 2175  ⟨cop 3635   class class class wbr 4043  Rcnr 7392  0_Rc0r 7393   <_R cltr 7398  ℝcr 7906   <_ℝ cltrr 7911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-coll 4158  ax-sep 4161  ax-nul 4169  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-iinf 4634

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-csb 3093  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-iun 3928  df-br 4044  df-opab 4105  df-mpt 4106  df-tr 4142  df-eprel 4334  df-id 4338  df-po 4341  df-iso 4342  df-iord 4411  df-on 4413  df-suc 4416  df-iom 4637  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-rn 4684  df-res 4685  df-ima 4686  df-iota 5229  df-fun 5270  df-fn 5271  df-f 5272  df-f1 5273  df-fo 5274  df-f1o 5275  df-fv 5276  df-ov 5937  df-oprab 5938  df-mpo 5939  df-1st 6216  df-2nd 6217  df-recs 6381  df-irdg 6446  df-1o 6492  df-oadd 6496  df-omul 6497  df-er 6610  df-ec 6612  df-qs 6616  df-ni 7399  df-pli 7400  df-mi 7401  df-lti 7402  df-plpq 7439  df-mpq 7440  df-enq 7442  df-nqqs 7443  df-plqqs 7444  df-mqqs 7445  df-1nqqs 7446  df-rq 7447  df-ltnqqs 7448  df-inp 7561  df-i1p 7562  df-enr 7821  df-nr 7822  df-ltr 7825  df-0r 7826  df-r 7917  df-lt 7920

This theorem is referenced by:  ltresr2  7935  pitoregt0  7944  ltrennb  7949  ax0lt1  7971  axprecex  7975  axpre-ltirr  7977  axpre-ltwlin  7978  axpre-lttrn  7979  axpre-apti  7980  axpre-ltadd  7981  axpre-mulgt0  7982  axpre-mulext  7983  axarch  7986  axcaucvglemcau  7993  axcaucvglemres  7994  axpre-suploclemres  7996