Theorem lenlts 28114

Description: Surreal less-than or equal in terms of less-than. (Contributed by Scott Fenton, 8-Dec-2021.)

Assertion

Ref	Expression
lenlts	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))

Proof of Theorem lenlts

Step	Hyp	Ref	Expression
1		df-les 28107	. . . 4 ⊢ ≤s = ((No × No) ∖ ◡ <s )
2	1	breqi 5108	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴((No × No) ∖ ◡ <s )𝐵)
3		brdif 5157	. . 3 ⊢ (𝐴((No × No) ∖ ◡ <s )𝐵 ↔ (𝐴(No × No)𝐵 ∧ ¬ 𝐴◡ <s 𝐵))
4		brxp 5699	. . . 4 ⊢ (𝐴(No × No)𝐵 ↔ (𝐴 ∈ No ∧ 𝐵 ∈ No))
5	4	anbi1i 636	. . 3 ⊢ ((𝐴(No × No)𝐵 ∧ ¬ 𝐴◡ <s 𝐵) ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ ¬ 𝐴◡ <s 𝐵))
6	2, 3, 5	3bitri 300	. 2 ⊢ (𝐴 ≤s 𝐵 ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ ¬ 𝐴◡ <s 𝐵))
7		ibar 538	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (¬ 𝐴◡ <s 𝐵 ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ ¬ 𝐴◡ <s 𝐵)))
8		brcnvg 5856	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴◡ <s 𝐵 ↔ 𝐵 <s 𝐴))
9	8	notbid 321	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (¬ 𝐴◡ <s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
10	7, 9	bitr3d 284	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (((𝐴 ∈ No ∧ 𝐵 ∈ No) ∧ ¬ 𝐴◡ <s 𝐵) ↔ ¬ 𝐵 <s 𝐴))
11	6, 10	bitrid 286	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   ∖ cdif 4045   class class class wbr 5102   × cxp 5648  ^◡ccnv 5649  Nocsur 28002   <s clts 28003   ≤s cles 28106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-les 28107

This theorem is used by:  ltnles  28115  lesloe  28116  lestri3  28117  lesnltd  28118  ltlestr  28122  leltstr  28123  lestr  28124  lesid  28129  lestric  28130  ltlesd  28135  ltsrec  28192  ltslpss  28299  cofcutr  28315  lenegs  28437  lesubsubsbd  28477  lesubsubs2bd  28478  lesubsubs3bd  28479  lesubaddsd  28484  lemuls2d  28565  lemuls1d  28566  ltonold  28652  oncutlt  28655  onnolt  28657  onles  28659  om2noseqlt2  28691  n0fincut  28746  bdaypw2n0bndlem  28854  bdaypw2bnd  28856  bdayfinbndlem1  28858  z12bdaylem1  28861