Theorem lenlts 27732

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 27725	. . . 4 ⊢ ≤s = (( No × No ) ∖ ◡ <s )
2	1	breqi 5106	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ◡ <s )𝐵)
3		brdif 5153	. . 3 ⊢ (𝐴(( No × No ) ∖ ◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴◡ <s 𝐵))
4		brxp 5681	. . . 4 ⊢ (𝐴( No × No )𝐵 ↔ (𝐴 ∈ No ∧ 𝐵 ∈ No ))
5	4	anbi1i 625	. . 3 ⊢ ((𝐴( No × No )𝐵 ∧ ¬ 𝐴◡ <s 𝐵) ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵))
6	2, 3, 5	3bitri 297	. 2 ⊢ (𝐴 ≤s 𝐵 ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵))
7		ibar 528	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (¬ 𝐴◡ <s 𝐵 ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵)))
8		brcnvg 5836	. . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴◡ <s 𝐵 ↔ 𝐵 <s 𝐴))
9	8	notbid 318	. . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (¬ 𝐴◡ <s 𝐵 ↔ ¬ 𝐵 <s 𝐴))
10	7, 9	bitr3d 281	. 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵) ↔ ¬ 𝐵 <s 𝐴))
11	6, 10	bitrid 283	1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   ∖ cdif 3900   class class class wbr 5100   × cxp 5630  ^◡ccnv 5631   No csur 27619   <s clts 27620   ≤s cles 27724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-les 27725

This theorem is referenced by:  ltnles  27733  lesloe  27734  lestri3  27735  lesnltd  27736  ltlestr  27740  leltstr  27741  lestr  27742  lesid  27747  lestric  27748  ltlesd  27753  ltsrec  27809  ltslpss  27916  cofcutr  27932  lenegs  28054  lesubsubsbd  28094  lesubsubs2bd  28095  lesubsubs3bd  28096  lesubaddsd  28101  lemuls2d  28182  lemuls1d  28183  ltonold  28269  oncutlt  28272  onnolt  28274  onles  28276  om2noseqlt2  28308  n0fincut  28363  bdaypw2n0bndlem  28471  bdaypw2bnd  28473  bdayfinbndlem1  28475  z12bdaylem1  28478