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 27697

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 27690	. . . 4 ⊢ ≤s = (( No × No ) ∖ ^◡ <s )
2	1	breqi 5108	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ^◡ <s )𝐵)
3		brdif 5155	. . 3 ⊢ (𝐴(( No × No ) ∖ ^◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴^◡ <s 𝐵))
4		brxp 5680	. . . 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 5833	. . . 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 2109 ∖ cdif 3908 class class class wbr 5102 × cxp 5629 ^◡ccnv 5630 No csur 27584 <s cslt 27585 ≤s csle 27689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2701 ax-sep 5246 ax-nul 5256 ax-pr 5382

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2721 df-clel 2803 df-ral 3045 df-rex 3054 df-rab 3403 df-v 3446 df-dif 3914 df-un 3916 df-ss 3928 df-nul 4293 df-if 4485 df-sn 4586 df-pr 4588 df-op 4592 df-br 5103 df-opab 5165 df-xp 5637 df-cnv 5639 df-sle 27690

This theorem is referenced by: sltnle 27698 sleloe 27699 sletri3 27700 sltletr 27701 slelttr 27702 sletr 27703 slerflex 27708 sletric 27709 sltled 27714 sltrec 27767 sltlpss 27857 cofcutr 27872 sleneg 27992 slesubsubbd 28030 slesubsub2bd 28031 slesubsub3bd 28032 slesubaddd 28037 slemul2d 28117 slemul1d 28118 sltonold 28202 onscutlt 28205 onnolt 28207 om2noseqlt2 28234 n0sfincut 28286

W3C validator