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 27664

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 27657	. . . 4 ⊢ ≤s = (( No × No ) ∖ ^◡ <s )
2	1	breqi 5113	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ^◡ <s )𝐵)
3		brdif 5160	. . 3 ⊢ (𝐴(( No × No ) ∖ ^◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴^◡ <s 𝐵))
4		brxp 5687	. . . 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 5843	. . . 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 3911 class class class wbr 5107 × cxp 5636 ^◡ccnv 5637 No csur 27551 <s cslt 27552 ≤s csle 27656

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 5251 ax-nul 5261 ax-pr 5387

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 3406 df-v 3449 df-dif 3917 df-un 3919 df-ss 3931 df-nul 4297 df-if 4489 df-sn 4590 df-pr 4592 df-op 4596 df-br 5108 df-opab 5170 df-xp 5644 df-cnv 5646 df-sle 27657

This theorem is referenced by: sltnle 27665 sleloe 27666 sletri3 27667 sltletr 27668 slelttr 27669 sletr 27670 slerflex 27675 sletric 27676 sltled 27681 sltrec 27732 sltlpss 27819 cofcutr 27832 sleneg 27952 slesubsubbd 27990 slesubsub2bd 27991 slesubsub3bd 27992 slesubaddd 27997 slemul2d 28077 slemul1d 28078 sltonold 28162 onscutlt 28165 onnolt 28167 om2noseqlt2 28194 n0sfincut 28246

W3C validator