Metamath Proof Explorer

Theorem negsproplem6

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is the same age as B . (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 𝐵 )
negsproplem6.4 ⊢ ( 𝜑 → ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) )
Assertion negsproplem6 ( 𝜑 → ( -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 negsproplem6.4 ⊢ ( 𝜑 → ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) )
6 nodense ⊢ ( ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ ( ( bday ‘ 𝐴 ) = ( bday ‘ 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑑 ∈ No ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) )
7 2 3 5 4 6 syl22anc ⊢ ( 𝜑 → ∃ 𝑑 ∈ No ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) )
8 uncom ⊢ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) = ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) )
9 8 eleq2i ⊢ ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) ↔ ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) )
10 9 imbi1i ⊢ ( ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) ↔ ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
11 10 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 ‘ 𝑥 ) ) ) ) )
12 1 11 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐵 ) ∪ ( bday ‘ 𝐴 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
13 12 3 negsproplem3 ⊢ ( 𝜑 → ( ( -us ‘ 𝐵 ) ∈ No ∧ ( -us “ ( R ‘ 𝐵 ) ) <<s { ( -us ‘ 𝐵 ) } ∧ { ( -us ‘ 𝐵 ) } <<s ( -us “ ( L ‘ 𝐵 ) ) ) )
14 13 simp1d ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) ∈ No )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝐵 ) ∈ No )
16 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝑑 ∈ No )
18 0no ⊢ 0s ∈ No
19 18 a1i ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 0s ∈ No )
20 bday0 ⊢ ( bday ‘ 0s ) = ∅
21 20 uneq2i ⊢ ( ( bday ‘ 𝑑 ) ∪ ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑑 ) ∪ ∅ )
22 un0 ⊢ ( ( bday ‘ 𝑑 ) ∪ ∅ ) = ( bday ‘ 𝑑 )
23 21 22 eqtri ⊢ ( ( bday ‘ 𝑑 ) ∪ ( bday ‘ 0s ) ) = ( bday ‘ 𝑑 )
24 simprr1 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) )
25 elun1 ⊢ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) → ( bday ‘ 𝑑 ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
26 24 25 syl ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( bday ‘ 𝑑 ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
27 23 26 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( ( bday ‘ 𝑑 ) ∪ ( bday ‘ 0s ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
28 16 17 19 27 negsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( ( -us ‘ 𝑑 ) ∈ No ∧ ( 𝑑 <s 0s → ( -us ‘ 0s ) <s ( -us ‘ 𝑑 ) ) ) )
29 28 simpld ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝑑 ) ∈ No )
30 1 2 negsproplem3 ⊢ ( 𝜑 → ( ( -us ‘ 𝐴 ) ∈ No ∧ ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } ∧ { ( -us ‘ 𝐴 ) } <<s ( -us “ ( L ‘ 𝐴 ) ) ) )
31 30 simp1d ⊢ ( 𝜑 → ( -us ‘ 𝐴 ) ∈ No )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝐴 ) ∈ No )
33 13 simp3d ⊢ ( 𝜑 → { ( -us ‘ 𝐵 ) } <<s ( -us “ ( L ‘ 𝐵 ) ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → { ( -us ‘ 𝐵 ) } <<s ( -us “ ( L ‘ 𝐵 ) ) )
35 fvex ⊢ ( -us ‘ 𝐵 ) ∈ V
36 35 snid ⊢ ( -us ‘ 𝐵 ) ∈ { ( -us ‘ 𝐵 ) }
37 36 a1i ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝐵 ) ∈ { ( -us ‘ 𝐵 ) } )
38 negsfn ⊢ -us Fn No
39 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
40 bdayon ⊢ ( bday ‘ 𝐴 ) ∈ On
41 oldbday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 𝑑 ∈ No ) → ( 𝑑 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ) )
42 40 17 41 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( 𝑑 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ) )
43 24 42 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝑑 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
44 5 fveq2d ⊢ ( 𝜑 → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐵 ) ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ( bday ‘ 𝐵 ) ) )
46 43 45 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝑑 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
47 simprr3 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝑑 <s 𝐵 )
48 elleft ⊢ ( 𝑑 ∈ ( L ‘ 𝐵 ) ↔ ( 𝑑 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) ∧ 𝑑 <s 𝐵 ) )
49 46 47 48 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝑑 ∈ ( L ‘ 𝐵 ) )
50 fnfvima ⊢ ( ( -us Fn No ∧ ( L ‘ 𝐵 ) ⊆ No ∧ 𝑑 ∈ ( L ‘ 𝐵 ) ) → ( -us ‘ 𝑑 ) ∈ ( -us “ ( L ‘ 𝐵 ) ) )
51 38 39 49 50 mp3an12i ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝑑 ) ∈ ( -us “ ( L ‘ 𝐵 ) ) )
52 34 37 51 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝑑 ) )
53 30 simp2d ⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us “ ( R ‘ 𝐴 ) ) <<s { ( -us ‘ 𝐴 ) } )
55 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
56 simprr2 ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝐴 <s 𝑑 )
57 elright ⊢ ( 𝑑 ∈ ( R ‘ 𝐴 ) ↔ ( 𝑑 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 𝐴 <s 𝑑 ) )
58 43 56 57 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → 𝑑 ∈ ( R ‘ 𝐴 ) )
59 fnfvima ⊢ ( ( -us Fn No ∧ ( R ‘ 𝐴 ) ⊆ No ∧ 𝑑 ∈ ( R ‘ 𝐴 ) ) → ( -us ‘ 𝑑 ) ∈ ( -us “ ( R ‘ 𝐴 ) ) )
60 38 55 58 59 mp3an12i ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝑑 ) ∈ ( -us “ ( R ‘ 𝐴 ) ) )
61 fvex ⊢ ( -us ‘ 𝐴 ) ∈ V
62 61 snid ⊢ ( -us ‘ 𝐴 ) ∈ { ( -us ‘ 𝐴 ) }
63 62 a1i ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝐴 ) ∈ { ( -us ‘ 𝐴 ) } )
64 54 60 63 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝑑 ) <s ( -us ‘ 𝐴 ) )
65 15 29 32 52 64 ltstrd ⊢ ( ( 𝜑 ∧ ( 𝑑 ∈ No ∧ ( ( bday ‘ 𝑑 ) ∈ ( bday ‘ 𝐴 ) ∧ 𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵 ) ) ) → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )
66 7 65 rexlimddv ⊢ ( 𝜑 → ( -us ‘ 𝐵 ) <s ( -us ‘ 𝐴 ) )