Theorem lenlts 27996

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 27989	. . . 4 ⊢ ≤s = (( No × No ) ∖ ◡ <s )
2	1	breqi 5113	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ◡ <s )𝐵)
3		brdif 5162	. . 3 ⊢ (𝐴(( No × No ) ∖ ◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴◡ <s 𝐵))
4		brxp 5708	. . . 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 5863	. . . 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 2145   ∖ cdif 3899   class class class wbr 5107   × cxp 5657  ^◡ccnv 5658   No csur 27884   <s clts 27885   ≤s cles 27988

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-xp 5665  df-cnv 5667  df-les 27989

This theorem is used by:  ltnles  27997  lesloe  27998  lestri3  27999  lesnltd  28000  ltlestr  28004  leltstr  28005  lestr  28006  lesid  28011  lestric  28012  ltlesd  28017  ltsrec  28074  ltslpss  28181  cofcutr  28197  lenegs  28319  lesubsubsbd  28359  lesubsubs2bd  28360  lesubsubs3bd  28361  lesubaddsd  28366  lemuls2d  28447  lemuls1d  28448  ltonold  28534  oncutlt  28537  onnolt  28539  onles  28541  om2noseqlt2  28573  n0fincut  28628  bdaypw2n0bndlem  28736  bdaypw2bnd  28738  bdayfinbndlem1  28740  z12bdaylem1  28743