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

Theorem xrlenlt 8020
Description: 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.)
Assertion
Ref Expression
xrlenlt ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))

Proof of Theorem xrlenlt
StepHypRef Expression
1 df-br 4004 . . 3 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≤ )
2 opelxpi 4658 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → ⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*))
3 df-le 7996 . . . . . . 7 ≤ = ((ℝ* × ℝ*) ∖ < )
43eleq2i 2244 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ))
5 eldif 3138 . . . . . 6 (⟨𝐴, 𝐵⟩ ∈ ((ℝ* × ℝ*) ∖ < ) ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
64, 5bitri 184 . . . . 5 (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
76baib 919 . . . 4 (⟨𝐴, 𝐵⟩ ∈ (ℝ* × ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
82, 7syl 14 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ ≤ ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
91, 8bitrid 192 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
10 df-br 4004 . . . 4 (𝐵 < 𝐴 ↔ ⟨𝐵, 𝐴⟩ ∈ < )
11 opelcnvg 4807 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (⟨𝐴, 𝐵⟩ ∈ < ↔ ⟨𝐵, 𝐴⟩ ∈ < ))
1210, 11bitr4id 199 . . 3 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐵 < 𝐴 ↔ ⟨𝐴, 𝐵⟩ ∈ < ))
1312notbid 667 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (¬ 𝐵 < 𝐴 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ < ))
149, 13bitr4d 191 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wcel 2148  cdif 3126  cop 3595   class class class wbr 4003   × cxp 4624  ccnv 4625  *cxr 7989   < clt 7990  cle 7991
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-le 7996
This theorem is referenced by:  lenlt  8031  pnfge  9787  mnfle  9790  xrltle  9796  xrleid  9798  xnn0dcle  9800  xrletri3  9802  xrlelttr  9804  xrltletr  9805  xrletr  9806  xgepnf  9814  xleneg  9835  xltadd1  9874  xsubge0  9879  xleaddadd  9885  iccid  9923  icc0r  9924  icodisj  9990  ioodisj  9991  ioo0  10257  ico0  10259  ioc0  10260  leisorel  10812  xrmaxleim  11247  xrmaxiflemval  11253  xrmaxlesup  11262  xrmaxaddlem  11263  xrminmax  11268  pcadd  12333  bldisj  13794  bdxmet  13894  bdbl  13896
  Copyright terms: Public domain W3C validator