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 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
negsproplem4.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
negsproplem4.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
negsproplem4.3 ⊢ ( 𝜑 → 𝐴 <s 𝐵 )
negsproplem5.4 ⊢ ( 𝜑 → ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) )
Assertion negsproplem5 ( 𝜑 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 negsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
2 negsproplem4.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 negsproplem4.2 ⊢ ( 𝜑 → 𝐵 ∈ No )
4 negsproplem4.3 ⊢ ( 𝜑 → 𝐴 <s 𝐵 )
5 negsproplem5.4 ⊢ ( 𝜑 → ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) )
6 1 2 negsproplem3 ⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } ∧ { ( -us ‘ 𝐴 ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )
7 6 simp2d ⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } )
8 negsfn ⊢ -us Fn No
9 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
10 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
11 oldbday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ No ) → ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
12 10 3 11 sylancr ⊢ ( 𝜑 → ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
13 5 12 mpbird ⊢ ( 𝜑 → 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
14 breq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 <s 𝑏 ↔ 𝐴 <s 𝐵 ) )
15 rightval ⊢ ( R ‘ 𝐴 ) = { 𝑏 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑏 }
16 14 15 elrab2 ⊢ ( 𝐵 ∈ ( R ‘ 𝐴 ) ↔ ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝐵 ) )
17 13 4 16 sylanbrc ⊢ ( 𝜑 → 𝐵 ∈ ( R ‘ 𝐴 ) )
18 fnfvima ⊢ ( ( -us Fn No ∧ ( R ‘ 𝐴 ) ⊆ No ∧ 𝐵 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝐵 ) ∈ ( -us “ ( R ‘ 𝐴 ) ) )
19 8 9 17 18 mp3an12i ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ ( -us “ ( R ‘ 𝐴 ) ) )
20 fvex ⊢ ( -us ‘ 𝐴 ) ∈ V
21 20 snid ⊢ ( -us ‘ 𝐴 ) ∈ { ( -us ‘ 𝐴 ) }
22 21 a1i ⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ { ( -us ‘ 𝐴 ) } )
23 7 19 22 ssltsepcd ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )