Metamath Proof Explorer

Theorem negsproplem3

Description: Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses negsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
negsproplem2.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
Assertion negsproplem3 ( 𝜑 → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } ∧ { ( -us ‘ 𝐴 ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 negsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
2 negsproplem2.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
3 1 2 negsproplem2 ⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) <<s ( -us “ ( L ‘ 𝐴 ) ) )
4 cutcuts ⊢ ( ( -us “ ( R ‘ 𝐴 ) ) <<s ( -us “ ( L ‘ 𝐴 ) ) → ( ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } ∧ { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )
5 3 4 syl ⊢ ( 𝜑 → ( ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } ∧ { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )
6 negsval ⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )
7 2 6 syl ⊢ ( 𝜑 → ( -us ‘ 𝐴 ) = ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) )
8 7 eleq1d ⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ∈ No ↔ ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) ∈ No ) )
9 7 sneqd ⊢ ( 𝜑 → { ( -us ‘ 𝐴 ) } = { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } )
10 9 breq2d ⊢ ( 𝜑 → ( ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } ↔ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } ) )
11 9 breq1d ⊢ ( 𝜑 → ( { ( -us ‘ 𝐴 ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ↔ { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )
12 8 10 11 3anbi123d ⊢ ( 𝜑 → ( ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } ∧ { ( -us ‘ 𝐴 ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) ↔ ( ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } ∧ { ( ( -us “ ( R ‘ 𝐴 ) ) |s ( -us “ ( L ‘ 𝐴 ) ) ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) ) )
13 5 12 mpbird ⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } ∧ { ( -us ‘ 𝐴 ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )