ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltresr GIF version

Theorem ltresr 7374
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.
StepHypRef Expression
1 ltrelre 7368 . . . 4 < ⊆ (ℝ × ℝ)
21brel 4490 . . 3 (⟨𝐴, 0R⟩ <𝐵, 0R⟩ → (⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ))
3 opelreal 7363 . . . 4 (⟨𝐴, 0R⟩ ∈ ℝ ↔ 𝐴R)
4 opelreal 7363 . . . 4 (⟨𝐵, 0R⟩ ∈ ℝ ↔ 𝐵R)
53, 4anbi12i 448 . . 3 ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) ↔ (𝐴R𝐵R))
62, 5sylib 120 . 2 (⟨𝐴, 0R⟩ <𝐵, 0R⟩ → (𝐴R𝐵R))
7 ltrelsr 7282 . . 3 <R ⊆ (R × R)
87brel 4490 . 2 (𝐴 <R 𝐵 → (𝐴R𝐵R))
9 eleq1 2150 . . . . . . . . 9 (𝑥 = ⟨𝐴, 0R⟩ → (𝑥 ∈ ℝ ↔ ⟨𝐴, 0R⟩ ∈ ℝ))
109anbi1d 453 . . . . . . . 8 (𝑥 = ⟨𝐴, 0R⟩ → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ)))
11 eqeq1 2094 . . . . . . . . . . 11 (𝑥 = ⟨𝐴, 0R⟩ → (𝑥 = ⟨𝑧, 0R⟩ ↔ ⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩))
1211anbi1d 453 . . . . . . . . . 10 (𝑥 = ⟨𝐴, 0R⟩ → ((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ↔ (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩)))
1312anbi1d 453 . . . . . . . . 9 (𝑥 = ⟨𝐴, 0R⟩ → (((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
14132exbidv 1796 . . . . . . . 8 (𝑥 = ⟨𝐴, 0R⟩ → (∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
1510, 14anbi12d 457 . . . . . . 7 (𝑥 = ⟨𝐴, 0R⟩ → (((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)) ↔ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))))
16 eleq1 2150 . . . . . . . . 9 (𝑦 = ⟨𝐵, 0R⟩ → (𝑦 ∈ ℝ ↔ ⟨𝐵, 0R⟩ ∈ ℝ))
1716anbi2d 452 . . . . . . . 8 (𝑦 = ⟨𝐵, 0R⟩ → ((⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ↔ (⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ)))
18 eqeq1 2094 . . . . . . . . . . 11 (𝑦 = ⟨𝐵, 0R⟩ → (𝑦 = ⟨𝑤, 0R⟩ ↔ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩))
1918anbi2d 452 . . . . . . . . . 10 (𝑦 = ⟨𝐵, 0R⟩ → ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ↔ (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩)))
2019anbi1d 453 . . . . . . . . 9 (𝑦 = ⟨𝐵, 0R⟩ → (((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
21202exbidv 1796 . . . . . . . 8 (𝑦 = ⟨𝐵, 0R⟩ → (∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
2217, 21anbi12d 457 . . . . . . 7 (𝑦 = ⟨𝐵, 0R⟩ → (((⟨𝐴, 0R⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)) ↔ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) ∧ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))))
23 df-lt 7361 . . . . . . 7 < = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∃𝑧𝑤((𝑥 = ⟨𝑧, 0R⟩ ∧ 𝑦 = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))}
2415, 22, 23brabg 4096 . . . . . 6 ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) → (⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) ∧ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤))))
2524bianabs 578 . . . . 5 ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) → (⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ ∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤)))
26 vex 2622 . . . . . . . . . . 11 𝑧 ∈ V
2726eqresr 7371 . . . . . . . . . 10 (⟨𝑧, 0R⟩ = ⟨𝐴, 0R⟩ ↔ 𝑧 = 𝐴)
28 eqcom 2090 . . . . . . . . . 10 (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ↔ ⟨𝑧, 0R⟩ = ⟨𝐴, 0R⟩)
29 eqcom 2090 . . . . . . . . . 10 (𝐴 = 𝑧𝑧 = 𝐴)
3027, 28, 293bitr4i 210 . . . . . . . . 9 (⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ↔ 𝐴 = 𝑧)
31 vex 2622 . . . . . . . . . . 11 𝑤 ∈ V
3231eqresr 7371 . . . . . . . . . 10 (⟨𝑤, 0R⟩ = ⟨𝐵, 0R⟩ ↔ 𝑤 = 𝐵)
33 eqcom 2090 . . . . . . . . . 10 (⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩ ↔ ⟨𝑤, 0R⟩ = ⟨𝐵, 0R⟩)
34 eqcom 2090 . . . . . . . . . 10 (𝐵 = 𝑤𝑤 = 𝐵)
3532, 33, 343bitr4i 210 . . . . . . . . 9 (⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩ ↔ 𝐵 = 𝑤)
3630, 35anbi12i 448 . . . . . . . 8 ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ↔ (𝐴 = 𝑧𝐵 = 𝑤))
3726, 31opth2 4067 . . . . . . . 8 (⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ↔ (𝐴 = 𝑧𝐵 = 𝑤))
3836, 37bitr4i 185 . . . . . . 7 ((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩)
3938anbi1i 446 . . . . . 6 (((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))
40392exbii 1542 . . . . 5 (∃𝑧𝑤((⟨𝐴, 0R⟩ = ⟨𝑧, 0R⟩ ∧ ⟨𝐵, 0R⟩ = ⟨𝑤, 0R⟩) ∧ 𝑧 <R 𝑤) ↔ ∃𝑧𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤))
4125, 40syl6bb 194 . . . 4 ((⟨𝐴, 0R⟩ ∈ ℝ ∧ ⟨𝐵, 0R⟩ ∈ ℝ) → (⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ ∃𝑧𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)))
423, 4, 41syl2anbr 286 . . 3 ((𝐴R𝐵R) → (⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ ∃𝑧𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤)))
43 breq12 3850 . . . 4 ((𝑧 = 𝐴𝑤 = 𝐵) → (𝑧 <R 𝑤𝐴 <R 𝐵))
4443copsex2g 4073 . . 3 ((𝐴R𝐵R) → (∃𝑧𝑤(⟨𝐴, 𝐵⟩ = ⟨𝑧, 𝑤⟩ ∧ 𝑧 <R 𝑤) ↔ 𝐴 <R 𝐵))
4542, 44bitrd 186 . 2 ((𝐴R𝐵R) → (⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ 𝐴 <R 𝐵))
466, 8, 45pm5.21nii 655 1 (⟨𝐴, 0R⟩ <𝐵, 0R⟩ ↔ 𝐴 <R 𝐵)
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1289  wex 1426  wcel 1438  cop 3449   class class class wbr 3845  Rcnr 6854  0Rc0r 6855   <R cltr 6860  cr 7347   < cltrr 7352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-coll 3954  ax-sep 3957  ax-nul 3965  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-iinf 4403
This theorem depends on definitions:  df-bi 115  df-dc 781  df-3or 925  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-nul 3287  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-int 3689  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-tr 3937  df-eprel 4116  df-id 4120  df-po 4123  df-iso 4124  df-iord 4193  df-on 4195  df-suc 4198  df-iom 4406  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-f1 5020  df-fo 5021  df-f1o 5022  df-fv 5023  df-ov 5655  df-oprab 5656  df-mpt2 5657  df-1st 5911  df-2nd 5912  df-recs 6070  df-irdg 6135  df-1o 6181  df-oadd 6185  df-omul 6186  df-er 6290  df-ec 6292  df-qs 6296  df-ni 6861  df-pli 6862  df-mi 6863  df-lti 6864  df-plpq 6901  df-mpq 6902  df-enq 6904  df-nqqs 6905  df-plqqs 6906  df-mqqs 6907  df-1nqqs 6908  df-rq 6909  df-ltnqqs 6910  df-inp 7023  df-i1p 7024  df-enr 7270  df-nr 7271  df-ltr 7274  df-0r 7275  df-r 7358  df-lt 7361
This theorem is referenced by:  ltresr2  7375  pitoregt0  7384  ltrennb  7389  ax0lt1  7409  axprecex  7413  axpre-ltirr  7415  axpre-ltwlin  7416  axpre-lttrn  7417  axpre-apti  7418  axpre-ltadd  7419  axpre-mulgt0  7420  axpre-mulext  7421  axarch  7424  axcaucvglemcau  7431  axcaucvglemres  7432
  Copyright terms: Public domain W3C validator