Metamath Proof Explorer


Theorem negsproplem7

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 3-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
Assertion negsproplem7 φ + 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 bdayelon bday A On
6 5 onordi Ord bday A
7 bdayelon bday B On
8 7 onordi Ord bday B
9 ordtri3or Ord bday A Ord bday B bday A bday B bday A = bday B bday B bday A
10 6 8 9 mp2an bday A bday B bday A = bday B bday B bday A
11 1 adantr φ bday A bday B x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
12 2 adantr φ bday A bday B A No
13 3 adantr φ bday A bday B B No
14 4 adantr φ bday A bday B A < s B
15 simpr φ bday A bday B bday A bday B
16 11 12 13 14 15 negsproplem4 φ bday A bday B + s B < s + s A
17 16 ex φ bday A bday B + s B < s + s A
18 1 adantr φ bday A = bday B x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
19 2 adantr φ bday A = bday B A No
20 3 adantr φ bday A = bday B B No
21 4 adantr φ bday A = bday B A < s B
22 simpr φ bday A = bday B bday A = bday B
23 18 19 20 21 22 negsproplem6 φ bday A = bday B + s B < s + s A
24 23 ex φ bday A = bday B + s B < s + s A
25 1 adantr φ bday B bday A x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x
26 2 adantr φ bday B bday A A No
27 3 adantr φ bday B bday A B No
28 4 adantr φ bday B bday A A < s B
29 simpr φ bday B bday A bday B bday A
30 25 26 27 28 29 negsproplem5 φ bday B bday A + s B < s + s A
31 30 ex φ bday B bday A + s B < s + s A
32 17 24 31 3jaod φ bday A bday B bday A = bday B bday B bday A + s B < s + s A
33 10 32 mpi φ + s B < s + s A