Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brsslt Structured version   Visualization version   GIF version

Theorem brsslt 32226
Description: Binary relation form of the surreal set less-than relation. (Contributed by Scott Fenton, 8-Dec-2021.)
Assertion
Ref Expression
brsslt (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 No 𝐵 No ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦)))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem brsslt
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-sslt 32223 . . 3 <<s = {⟨𝑎, 𝑏⟩ ∣ (𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦)}
21bropaex12 5401 . 2 (𝐴 <<s 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3 sseq1 3830 . . . 4 (𝑎 = 𝐴 → (𝑎 No 𝐴 No ))
4 raleq 3334 . . . 4 (𝑎 = 𝐴 → (∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦 ↔ ∀𝑥𝐴𝑦𝑏 𝑥 <s 𝑦))
53, 43anbi13d 1555 . . 3 (𝑎 = 𝐴 → ((𝑎 No 𝑏 No ∧ ∀𝑥𝑎𝑦𝑏 𝑥 <s 𝑦) ↔ (𝐴 No 𝑏 No ∧ ∀𝑥𝐴𝑦𝑏 𝑥 <s 𝑦)))
6 sseq1 3830 . . . 4 (𝑏 = 𝐵 → (𝑏 No 𝐵 No ))
7 raleq 3334 . . . . 5 (𝑏 = 𝐵 → (∀𝑦𝑏 𝑥 <s 𝑦 ↔ ∀𝑦𝐵 𝑥 <s 𝑦))
87ralbidv 3181 . . . 4 (𝑏 = 𝐵 → (∀𝑥𝐴𝑦𝑏 𝑥 <s 𝑦 ↔ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦))
96, 83anbi23d 1556 . . 3 (𝑏 = 𝐵 → ((𝐴 No 𝑏 No ∧ ∀𝑥𝐴𝑦𝑏 𝑥 <s 𝑦) ↔ (𝐴 No 𝐵 No ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦)))
105, 9, 1brabg 5196 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 <<s 𝐵 ↔ (𝐴 No 𝐵 No ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦)))
112, 10biadan2 844 1 (𝐴 <<s 𝐵 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ (𝐴 No 𝐵 No ∧ ∀𝑥𝐴𝑦𝐵 𝑥 <s 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2157  wral 3103  Vcvv 3398  wss 3776   class class class wbr 4851   No csur 32119   <s cslt 32120   <<s csslt 32222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pr 5103
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-br 4852  df-opab 4914  df-xp 5324  df-sslt 32223
This theorem is referenced by:  ssltex1  32227  ssltex2  32228  ssltss1  32229  ssltss2  32230  ssltsep  32231  sssslt1  32232  sssslt2  32233  nulsslt  32234  nulssgt  32235  conway  32236  sslttr  32240  ssltun1  32241  ssltun2  32242  etasslt  32246  slerec  32249
  Copyright terms: Public domain W3C validator