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 bdayon ⊢ bday ⁡ A ∈ On
6 5 onordi ⊢ Ord ⁡ bday ⁡ A
7 bdayon ⊢ 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