Metamath Proof Explorer

Theorem negsproplem5

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when B is simpler than A . (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
negsproplem5.4 ⊢ φ → bday ⁡ B ∈ bday ⁡ A
Assertion negsproplem5 ⊢ φ → + 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 negsproplem5.4 ⊢ φ → bday ⁡ B ∈ bday ⁡ A
6 1 2 negsproplem3 ⊢ φ → + s ⁡ A ∈ No ∧ + s R ⁡ A ≪ s + s ⁡ A ∧ + s ⁡ A ≪ s + s L ⁡ A
7 6 simp2d ⊢ φ → + s R ⁡ A ≪ s + s ⁡ A
8 negsfn ⊢ + s Fn No
9 rightssno ⊢ R ⁡ A ⊆ No
10 bdayelon ⊢ bday ⁡ A ∈ On
11 oldbday ⊢ bday ⁡ A ∈ On ∧ B ∈ No → B ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ B ∈ bday ⁡ A
12 10 3 11 sylancr ⊢ φ → B ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ B ∈ bday ⁡ A
13 5 12 mpbird ⊢ φ → B ∈ Old ⁡ bday ⁡ A
14 elright ⊢ B ∈ R ⁡ A ↔ B ∈ Old ⁡ bday ⁡ A ∧ A < s B
15 13 4 14 sylanbrc ⊢ φ → B ∈ R ⁡ A
16 fnfvima ⊢ + s Fn No ∧ R ⁡ A ⊆ No ∧ B ∈ R ⁡ A → + s ⁡ B ∈ + s R ⁡ A
17 8 9 15 16 mp3an12i ⊢ φ → + s ⁡ B ∈ + s R ⁡ A
18 fvex ⊢ + s ⁡ A ∈ V
19 18 snid ⊢ + s ⁡ A ∈ + s ⁡ A
20 19 a1i ⊢ φ → + s ⁡ A ∈ + s ⁡ A
21 7 17 20 ssltsepcd ⊢ φ → + s ⁡ B < s + s ⁡ A