slenlt - Metamath Proof Explorer

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

Theorem slenlt 27691

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**
Step	Hyp	Ref	Expression
1		df-sle 27684	. . . 4 ⊢ ≤s = (( No × No ) ∖ ^◡ <s )
2	1	breqi 5095	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ^◡ <s )𝐵)
3		brdif 5142	. . 3 ⊢ (𝐴(( No × No ) ∖ ^◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴^◡ <s 𝐵))
4		brxp 5663	. . . 4 ⊢ (𝐴( No × No )𝐵 ↔ (𝐴 ∈ No ∧ 𝐵 ∈ No ))
5	4	anbi1i 624	. . 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 5818	. . . 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 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2111 ∖ cdif 3894 class class class wbr 5089 × cxp 5612 ^◡ccnv 5613 No csur 27578 <s cslt 27579 ≤s csle 27683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pr 5368

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-ss 3914 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-br 5090 df-opab 5152 df-xp 5620 df-cnv 5622 df-sle 27684

This theorem is referenced by: sltnle 27692 sleloe 27693 sletri3 27694 sltletr 27695 slelttr 27696 sletr 27697 slerflex 27702 sletric 27703 sltled 27708 sltrec 27762 sltlpss 27853 cofcutr 27868 sleneg 27988 slesubsubbd 28026 slesubsub2bd 28027 slesubsub3bd 28028 slesubaddd 28033 slemul2d 28113 slemul1d 28114 sltonold 28198 onscutlt 28201 onnolt 28203 om2noseqlt2 28230 n0sfincut 28282

W3C validator