Metamath Proof Explorer

Theorem negsproplem4

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is simpler than B . (Contributed by Scott Fenton, 2-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 𝐵 )
negsproplem4.4 ⊢ ( 𝜑 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )
Assertion negsproplem4 ( 𝜑 → ( -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 negsproplem4.4 ⊢ ( 𝜑 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )
6 uncom ⊢ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) = ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) )
7 6 eleq2i ⊢ ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ↔ ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) )
8 7 imbi1i ⊢ ( ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
9 8 2ralbii ⊢ ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
10 1 9 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
11 10 3 negsproplem3 ⊢ ( 𝜑 → ( ( -us ‘ 𝐵 ) ∈ No ∧ ( -us “ ( R ‘ 𝐵 ) ) <<s { ( -us ‘ 𝐵 ) } ∧ { ( -us ‘ 𝐵 ) } <<s ( -us “ ( L ‘ 𝐵 ) ) ) )
12 11 simp3d ⊢ ( 𝜑 → { ( -us ‘ 𝐵 ) } <<s ( -us “ ( L ‘ 𝐵 ) ) )
13 fvex ⊢ ( -us ‘ 𝐵 ) ∈ V
14 13 snid ⊢ ( -us ‘ 𝐵 ) ∈ { ( -us ‘ 𝐵 ) }
15 14 a1i ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ { ( -us ‘ 𝐵 ) } )
16 negsfn ⊢ -us Fn No
17 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
18 bdayelon ⊢ ( bday ‘ 𝐵 ) ∈ On
19 oldbday ⊢ ( ( ( bday ‘ 𝐵 ) ∈ On ∧ 𝐴 ∈ No ) → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ↔ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
20 18 2 19 sylancr ⊢ ( 𝜑 → ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ↔ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) )
21 5 20 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
22 breq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 <s 𝐵 ↔ 𝐴 <s 𝐵 ) )
23 leftval ⊢ ( L ‘ 𝐵 ) = { 𝑎 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ∣ 𝑎 <s 𝐵 }
24 22 23 elrab2 ⊢ ( 𝐴 ∈ ( L ‘ 𝐵 ) ↔ ( 𝐴 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ∧ 𝐴 <s 𝐵 ) )
25 21 4 24 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ ( L ‘ 𝐵 ) )
26 fnfvima ⊢ ( ( -us Fn No ∧ ( L ‘ 𝐵 ) ⊆ No ∧ 𝐴 ∈ ( L ‘ 𝐵 ) ) → ( -us ‘ 𝐴 ) ∈ ( -us “ ( L ‘ 𝐵 ) ) )
27 16 17 25 26 mp3an12i ⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ ( -us “ ( L ‘ 𝐵 ) ) )
28 12 15 27 ssltsepcd ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )