MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  slenlt Structured version   Visualization version   GIF version

Theorem slenlt 27255
Description: Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
slenlt ((𝐴 No 𝐵 No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))

Proof of Theorem slenlt
StepHypRef Expression
1 df-sle 27248 . . . 4 ≤s = (( No × No ) ∖ <s )
21breqi 5155 . . 3 (𝐴 ≤s 𝐵𝐴(( No × No ) ∖ <s )𝐵)
3 brdif 5202 . . 3 (𝐴(( No × No ) ∖ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴 <s 𝐵))
4 brxp 5726 . . . 4 (𝐴( No × No )𝐵 ↔ (𝐴 No 𝐵 No ))
54anbi1i 625 . . 3 ((𝐴( No × No )𝐵 ∧ ¬ 𝐴 <s 𝐵) ↔ ((𝐴 No 𝐵 No ) ∧ ¬ 𝐴 <s 𝐵))
62, 3, 53bitri 297 . 2 (𝐴 ≤s 𝐵 ↔ ((𝐴 No 𝐵 No ) ∧ ¬ 𝐴 <s 𝐵))
7 ibar 530 . . 3 ((𝐴 No 𝐵 No ) → (¬ 𝐴 <s 𝐵 ↔ ((𝐴 No 𝐵 No ) ∧ ¬ 𝐴 <s 𝐵)))
8 brcnvg 5880 . . . 4 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵𝐵 <s 𝐴))
98notbid 318 . . 3 ((𝐴 No 𝐵 No ) → (¬ 𝐴 <s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
107, 9bitr3d 281 . 2 ((𝐴 No 𝐵 No ) → (((𝐴 No 𝐵 No ) ∧ ¬ 𝐴 <s 𝐵) ↔ ¬ 𝐵 <s 𝐴))
116, 10bitrid 283 1 ((𝐴 No 𝐵 No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wcel 2107  cdif 3946   class class class wbr 5149   × cxp 5675  ccnv 5676   No csur 27143   <s cslt 27144   ≤s csle 27247
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-sle 27248
This theorem is referenced by:  sltnle  27256  sleloe  27257  sletri3  27258  sltletr  27259  slelttr  27260  sletr  27261  slerflex  27266  sletric  27267  sltled  27272  sltrec  27321  sltlpss  27401  cofcutr  27411  sleneg  27520  slesubsubbd  27553  slesubsub2bd  27554  slesubsub3bd  27555  slemul2d  27626  slemul1d  27627
  Copyright terms: Public domain W3C validator