![]() |
Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > slenlt | Structured version Visualization version GIF version |
Description: Surreal less than or equal in terms of less than. (Contributed by Scott Fenton, 8-Dec-2021.) |
Ref | Expression |
---|---|
slenlt | ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-sle 32745 | . . . 4 ⊢ ≤s = (( No × No ) ∖ ◡ <s ) | |
2 | 1 | breqi 4936 | . . 3 ⊢ (𝐴 ≤s 𝐵 ↔ 𝐴(( No × No ) ∖ ◡ <s )𝐵) |
3 | brdif 4983 | . . 3 ⊢ (𝐴(( No × No ) ∖ ◡ <s )𝐵 ↔ (𝐴( No × No )𝐵 ∧ ¬ 𝐴◡ <s 𝐵)) | |
4 | brxp 5454 | . . . 4 ⊢ (𝐴( No × No )𝐵 ↔ (𝐴 ∈ No ∧ 𝐵 ∈ No )) | |
5 | 4 | anbi1i 614 | . . 3 ⊢ ((𝐴( No × No )𝐵 ∧ ¬ 𝐴◡ <s 𝐵) ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵)) |
6 | 2, 3, 5 | 3bitri 289 | . 2 ⊢ (𝐴 ≤s 𝐵 ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵)) |
7 | ibar 521 | . . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (¬ 𝐴◡ <s 𝐵 ↔ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵))) | |
8 | brcnvg 5601 | . . . 4 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴◡ <s 𝐵 ↔ 𝐵 <s 𝐴)) | |
9 | 8 | notbid 310 | . . 3 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (¬ 𝐴◡ <s 𝐵 ↔ ¬ 𝐵 <s 𝐴)) |
10 | 7, 9 | bitr3d 273 | . 2 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ¬ 𝐴◡ <s 𝐵) ↔ ¬ 𝐵 <s 𝐴)) |
11 | 6, 10 | syl5bb 275 | 1 ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ¬ 𝐵 <s 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∈ wcel 2050 ∖ cdif 3828 class class class wbr 4930 × cxp 5406 ◡ccnv 5407 No csur 32668 <s cslt 32669 ≤s csle 32744 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pr 5187 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-br 4931 df-opab 4993 df-xp 5414 df-cnv 5416 df-sle 32745 |
This theorem is referenced by: sltnle 32753 sleloe 32754 sletri3 32755 sltletr 32756 slelttr 32757 sletr 32758 sltrec 32799 |
Copyright terms: Public domain | W3C validator |