Metamath Proof Explorer


Theorem negsproplem1

Description: Lemma for surreal negation. We prove a pair of properties of surreal negation simultaneously. First, we instantiate some quantifiers. (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
negsproplem1.1 φ X No
negsproplem1.2 φ Y No
negsproplem1.3 φ bday X bday Y bday A bday B
Assertion negsproplem1 φ + s X No X < s Y + s Y < s + s X

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 negsproplem1.1 φ X No
3 negsproplem1.2 φ Y No
4 negsproplem1.3 φ bday X bday Y bday A bday B
5 2 3 jca φ X No Y No
6 fveq2 x = X bday x = bday X
7 6 uneq1d x = X bday x bday y = bday X bday y
8 7 eleq1d x = X bday x bday y bday A bday B bday X bday y bday A bday B
9 fveq2 x = X + s x = + s X
10 9 eleq1d x = X + s x No + s X No
11 breq1 x = X x < s y X < s y
12 9 breq2d x = X + s y < s + s x + s y < s + s X
13 11 12 imbi12d x = X x < s y + s y < s + s x X < s y + s y < s + s X
14 10 13 anbi12d x = X + s x No x < s y + s y < s + s x + s X No X < s y + s y < s + s X
15 8 14 imbi12d x = X bday x bday y bday A bday B + s x No x < s y + s y < s + s x bday X bday y bday A bday B + s X No X < s y + s y < s + s X
16 fveq2 y = Y bday y = bday Y
17 16 uneq2d y = Y bday X bday y = bday X bday Y
18 17 eleq1d y = Y bday X bday y bday A bday B bday X bday Y bday A bday B
19 breq2 y = Y X < s y X < s Y
20 fveq2 y = Y + s y = + s Y
21 20 breq1d y = Y + s y < s + s X + s Y < s + s X
22 19 21 imbi12d y = Y X < s y + s y < s + s X X < s Y + s Y < s + s X
23 22 anbi2d y = Y + s X No X < s y + s y < s + s X + s X No X < s Y + s Y < s + s X
24 18 23 imbi12d y = Y bday X bday y bday A bday B + s X No X < s y + s y < s + s X bday X bday Y bday A bday B + s X No X < s Y + s Y < s + s X
25 15 24 rspc2v X No Y No x No y No bday x bday y bday A bday B + s x No x < s y + s y < s + s x bday X bday Y bday A bday B + s X No X < s Y + s Y < s + s X
26 5 1 4 25 syl3c φ + s X No X < s Y + s Y < s + s X