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		elright	⊢ ( 𝐵 ∈ ( R ‘ 𝐴 ) ↔ ( 𝐵 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝐵 ) )
15	13 4 14	sylanbrc	⊢ ( 𝜑 → 𝐵 ∈ ( R ‘ 𝐴 ) )
16		fnfvima	⊢ ( ( -us Fn No ∧ ( R ‘ 𝐴 ) ⊆ No ∧ 𝐵 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝐵 ) ∈ ( -us “ ( R ‘ 𝐴 ) ) )
17	8 9 15 16	mp3an12i	⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ ( -us “ ( R ‘ 𝐴 ) ) )
18		fvex	⊢ ( -us ‘ 𝐴 ) ∈ V
19	18	snid	⊢ ( -us ‘ 𝐴 ) ∈ { ( -us ‘ 𝐴 ) }
20	19	a1i	⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ { ( -us ‘ 𝐴 ) } )
21	7 17 20	ssltsepcd	⊢ ( 𝜑 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )