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 27722

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 27715	. . . 4 ⊢ ≤s = (( No × No ) ∖ ^◡ <s )
2	1	breqi 5103	. . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ^◡ <s )𝐵)
3		brdif 5150	. . 3 ⊢ (𝐴(( No × No ) ∖ ^◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴^◡ <s 𝐵))
4		brxp 5672	. . . 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 5827	. . . 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 2114 ∖ cdif 3897 class class class wbr 5097 × cxp 5621 ^◡ccnv 5622 No csur 27609 <s cslt 27610 ≤s csle 27714

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 2707 ax-sep 5240 ax-nul 5250 ax-pr 5376

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 2714 df-cleq 2727 df-clel 2810 df-ral 3051 df-rex 3060 df-rab 3399 df-v 3441 df-dif 3903 df-un 3905 df-ss 3917 df-nul 4285 df-if 4479 df-sn 4580 df-pr 4582 df-op 4586 df-br 5098 df-opab 5160 df-xp 5629 df-cnv 5631 df-sle 27715

This theorem is referenced by: sltnle 27723 sleloe 27724 sletri3 27725 slenltd 27726 sltletr 27730 slelttr 27731 sletr 27732 slerflex 27737 sletric 27738 sltled 27743 sltrec 27797 sltlpss 27888 cofcutr 27904 sleneg 28026 slesubsubbd 28066 slesubsub2bd 28067 slesubsub3bd 28068 slesubaddd 28073 slemul2d 28154 slemul1d 28155 sltonold 28240 onscutlt 28243 onnolt 28245 onsle 28247 om2noseqlt2 28279 n0sfincut 28333 bdaypw2n0sbndlem 28440 bdaypw2bnd 28442 bdayfinbndlem1 28444 zs12bdaylem1 28447

W3C validator