Metamath Proof Explorer


Theorem negsproplem4

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is simpler than B . (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses negsproplem.1 φ x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
negsproplem4.1 φ A No
negsproplem4.2 φ B No
negsproplem4.3 φ A < s B
negsproplem4.4 φ bday A bday B
Assertion negsproplem4 φ + s B < s + s A

Proof

Step Hyp Ref Expression
1 negsproplem.1 φ x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
2 negsproplem4.1 φ A No
3 negsproplem4.2 φ B No
4 negsproplem4.3 φ A < s B
5 negsproplem4.4 φ bday A bday B
6 uncom bday A bday B = bday B bday A
7 6 eleq2i bday x bday y bday A bday B bday x bday y bday B bday A
8 7 imbi1i bday x bday y bday A bday B + s x No x < s y + s y < s + s x bday x bday y bday B bday A + s x No x < s y + s y < s + s x
9 8 2ralbii x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x x No y No bday x bday y bday B bday A + s x No x < s y + s y < s + s x
10 1 9 sylib φ x No y No bday x bday y bday B bday A + s x No x < s y + s y < s + s x
11 10 3 negsproplem3 φ + s B No + s R B s + s B + s B s + s L B
12 11 simp3d φ + s B s + s L B
13 fvex + s B V
14 13 snid + s B + s B
15 14 a1i φ + s B + s B
16 negsfn + s Fn No
17 leftssno L B No
18 bdayelon bday B On
19 oldbday bday B On A No A Old bday B bday A bday B
20 18 2 19 sylancr φ A Old bday B bday A bday B
21 5 20 mpbird φ A Old bday B
22 breq1 a = A a < s B A < s B
23 leftval L B = a Old bday B | a < s B
24 22 23 elrab2 A L B A Old bday B A < s B
25 21 4 24 sylanbrc φ A L B
26 fnfvima + s Fn No L B No A L B + s A + s L B
27 16 17 25 26 mp3an12i φ + s A + s L B
28 12 15 27 ssltsepcd φ + s B < s + s A