Metamath Proof Explorer

Theorem negsproplem7

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis unconditionally. (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 𝐵 )
Assertion negsproplem7 ( 𝜑 → ( -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 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
6 5 onordi ⊢ Ord ( bday ‘ 𝐴 )
7 bdayelon ⊢ ( bday ‘ 𝐵 ) ∈ On
8 7 onordi ⊢ Ord ( bday ‘ 𝐵 )
9 ordtri3or ⊢ ( ( Ord ( bday ‘ 𝐴 ) ∧ Ord ( bday ‘ 𝐵 ) ) → ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ∨ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∨ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) )
10 6 8 9 mp2an ⊢ ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ∨ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∨ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
12 2 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) → 𝐴 ∈ No )
13 3 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) → 𝐵 ∈ No )
14 4 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) → 𝐴 <s 𝐵 )
15 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) )
16 11 12 13 14 15 negsproplem4 ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )
17 16 ex ⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
18 1 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
19 2 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐴 ∈ No )
20 3 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐵 ∈ No )
21 4 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → 𝐴 <s 𝐵 )
22 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) )
23 18 19 20 21 22 negsproplem6 ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )
24 23 ex ⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
25 1 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
26 2 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐴 ∈ No )
27 3 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐵 ∈ No )
28 4 adantr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → 𝐴 <s 𝐵 )
29 simpr ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) )
30 25 26 27 28 29 negsproplem5 ⊢ ( ( 𝜑 ∧ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )
31 30 ex ⊢ ( 𝜑 → ( ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
32 17 24 31 3jaod ⊢ ( 𝜑 → ( ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝐵 ) ∨ ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∨ ( bday ‘ 𝐵 ) ∈ ( bday ‘ 𝐴 ) ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) ) )
33 10 32 mpi ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )