Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nomaxmo Structured version   Visualization version   GIF version

Theorem nomaxmo 33326
 Description: A class of surreals has at most one maximum. (Contributed by Scott Fenton, 5-Dec-2021.)
Assertion
Ref Expression
nomaxmo (𝑆 No → ∃*𝑥𝑆𝑦𝑆 ¬ 𝑥 <s 𝑦)
Distinct variable group:   𝑥,𝑆,𝑦

Proof of Theorem nomaxmo
StepHypRef Expression
1 sltso 33306 . . . . 5 <s Or No
2 soss 5457 . . . . 5 (𝑆 No → ( <s Or No → <s Or 𝑆))
31, 2mpi 20 . . . 4 (𝑆 No → <s Or 𝑆)
4 cnvso 6107 . . . 4 ( <s Or 𝑆 <s Or 𝑆)
53, 4sylib 221 . . 3 (𝑆 No <s Or 𝑆)
6 somo 5474 . . 3 ( <s Or 𝑆 → ∃*𝑥𝑆𝑦𝑆 ¬ 𝑦 <s 𝑥)
75, 6syl 17 . 2 (𝑆 No → ∃*𝑥𝑆𝑦𝑆 ¬ 𝑦 <s 𝑥)
8 vex 3444 . . . . . 6 𝑦 ∈ V
9 vex 3444 . . . . . 6 𝑥 ∈ V
108, 9brcnv 5717 . . . . 5 (𝑦 <s 𝑥𝑥 <s 𝑦)
1110notbii 323 . . . 4 𝑦 <s 𝑥 ↔ ¬ 𝑥 <s 𝑦)
1211ralbii 3133 . . 3 (∀𝑦𝑆 ¬ 𝑦 <s 𝑥 ↔ ∀𝑦𝑆 ¬ 𝑥 <s 𝑦)
1312rmobii 3349 . 2 (∃*𝑥𝑆𝑦𝑆 ¬ 𝑦 <s 𝑥 ↔ ∃*𝑥𝑆𝑦𝑆 ¬ 𝑥 <s 𝑦)
147, 13sylib 221 1 (𝑆 No → ∃*𝑥𝑆𝑦𝑆 ¬ 𝑥 <s 𝑦)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∀wral 3106  ∃*wrmo 3109   ⊆ wss 3881   class class class wbr 5030   Or wor 5437  ◡ccnv 5518   No csur 33272
 Copyright terms: Public domain W3C validator