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 breq2 ⊢ b = B → A < s b ↔ A < s B
15 rightval ⊢ R ⁡ A = b ∈ Old ⁡ bday ⁡ A | A < s b
16 14 15 elrab2 ⊢ B ∈ R ⁡ A ↔ B ∈ Old ⁡ bday ⁡ A ∧ A < s B
17 13 4 16 sylanbrc ⊢ φ → B ∈ R ⁡ A
18 fnfvima ⊢ + s Fn No ∧ R ⁡ A ⊆ No ∧ B ∈ R ⁡ A → + s ⁡ B ∈ + s R ⁡ A
19 8 9 17 18 mp3an12i ⊢ φ → + s ⁡ B ∈ + s R ⁡ A
20 fvex ⊢ + s ⁡ A ∈ V
21 20 snid ⊢ + s ⁡ A ∈ + s ⁡ A
22 21 a1i ⊢ φ → + s ⁡ A ∈ + s ⁡ A
23 7 19 22 ssltsepcd ⊢ φ → + s ⁡ B < s + s ⁡ A