Metamath Proof Explorer

Theorem negsproplem2

Description: Lemma for surreal negation. Show that the cut that defines negation is legitimate. (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 negsproplem2 ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) <<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 negsfn ⊢ -us Fn No
4 fnfun ⊢ ( -us Fn No → Fun -us )
5 3 4 ax-mp ⊢ Fun -us
6 fvex ⊢ ( R ‘ 𝐴 ) ∈ V
7 6 funimaex ⊢ ( Fun -us → ( -us “ ( R ‘ 𝐴 ) ) ∈ V )
8 5 7 mp1i ⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) ∈ V )
9 fvex ⊢ ( L ‘ 𝐴 ) ∈ V
10 9 funimaex ⊢ ( Fun -us → ( -us “ ( L ‘ 𝐴 ) ) ∈ V )
11 5 10 mp1i ⊢ ( 𝜑 → ( -us “ ( L ‘ 𝐴 ) ) ∈ V )
12 rightssold ⊢ ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
13 imass2 ⊢ ( ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) → ( -us “ ( R ‘ 𝐴 ) ) ⊆ ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) ) )
14 12 13 ax-mp ⊢ ( -us “ ( R ‘ 𝐴 ) ) ⊆ ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
16 oldssno ⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ No
17 16 sseli ⊢ ( 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → 𝑎 ∈ No )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → 𝑎 ∈ No )
19 0sno ⊢ 0s ∈ No
20 19 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → 0s ∈ No )
21 bday0s ⊢ ( bday ‘ 0s ) = ∅
22 21 uneq2i ⊢ ( ( bday ‘ 𝑎 ) ∪ ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑎 ) ∪ ∅ )
23 un0 ⊢ ( ( bday ‘ 𝑎 ) ∪ ∅ ) = ( bday ‘ 𝑎 )
24 22 23 eqtri ⊢ ( ( bday ‘ 𝑎 ) ∪ ( bday ‘ 0s ) ) = ( bday ‘ 𝑎 )
25 oldbdayim ⊢ ( 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝐴 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝐴 ) )
27 elun1 ⊢ ( ( bday ‘ 𝑎 ) ∈ ( bday ‘ 𝐴 ) → ( bday ‘ 𝑎 ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝑎 ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
29 24 28 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( ( bday ‘ 𝑎 ) ∪ ( bday ‘ 0s ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
30 15 18 20 29 negsproplem1 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝑎 ) ∈ No ∧ ( 𝑎 <s 0s → ( -us ‘ 0s ) <s ( -us ‘ 𝑎 ) ) ) )
31 30 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝑎 ) ∈ No )
32 31 ralrimiva ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ( -us ‘ 𝑎 ) ∈ No )
33 3 fndmi ⊢ dom -us = No
34 16 33 sseqtrri ⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ dom -us
35 funimass4 ⊢ ( ( Fun -us ∧ ( O ‘ ( bday ‘ 𝐴 ) ) ⊆ dom -us ) → ( ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) ) ⊆ No ↔ ∀ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ( -us ‘ 𝑎 ) ∈ No ) )
36 5 34 35 mp2an ⊢ ( ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) ) ⊆ No ↔ ∀ 𝑎 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ( -us ‘ 𝑎 ) ∈ No )
37 32 36 sylibr ⊢ ( 𝜑 → ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) ) ⊆ No )
38 14 37 sstrid ⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) ⊆ No )
39 leftssold ⊢ ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) )
40 imass2 ⊢ ( ( L ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) → ( -us “ ( L ‘ 𝐴 ) ) ⊆ ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) ) )
41 39 40 ax-mp ⊢ ( -us “ ( L ‘ 𝐴 ) ) ⊆ ( -us “ ( O ‘ ( bday ‘ 𝐴 ) ) )
42 41 37 sstrid ⊢ ( 𝜑 → ( -us “ ( L ‘ 𝐴 ) ) ⊆ No )
43 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
44 fvelimab ⊢ ( ( -us Fn No ∧ ( R ‘ 𝐴 ) ⊆ No ) → ( 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑥𝑅 ) = 𝑎 ) )
45 3 43 44 mp2an ⊢ ( 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑥𝑅 ) = 𝑎 )
46 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
47 fvelimab ⊢ ( ( -us Fn No ∧ ( L ‘ 𝐴 ) ⊆ No ) → ( 𝑏 ∈ ( -us “ ( L ‘ 𝐴 ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( -us ‘ 𝑥𝐿 ) = 𝑏 ) )
48 3 46 47 mp2an ⊢ ( 𝑏 ∈ ( -us “ ( L ‘ 𝐴 ) ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( -us ‘ 𝑥𝐿 ) = 𝑏 )
49 45 48 anbi12i ⊢ ( ( 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∧ 𝑏 ∈ ( -us “ ( L ‘ 𝐴 ) ) ) ↔ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( -us ‘ 𝑥𝐿 ) = 𝑏 ) )
50 reeanv ⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ( -us ‘ 𝑥𝐿 ) = 𝑏 ) ↔ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( -us ‘ 𝑥𝐿 ) = 𝑏 ) )
51 49 50 bitr4i ⊢ ( ( 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∧ 𝑏 ∈ ( -us “ ( L ‘ 𝐴 ) ) ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ( -us ‘ 𝑥𝐿 ) = 𝑏 ) )
52 lltropt ⊢ ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 )
53 52 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( L ‘ 𝐴 ) <<s ( R ‘ 𝐴 ) )
54 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝐿 ∈ ( L ‘ 𝐴 ) )
55 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝑅 ∈ ( R ‘ 𝐴 ) )
56 53 54 55 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝐿 <s 𝑥𝑅 )
57 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ( ( ( bday ‘ 𝑥 ) ∪ ( bday ‘ 𝑦 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) → ( ( -us ‘ 𝑥 ) ∈ No ∧ ( 𝑥 <s 𝑦 → ( -us ‘ 𝑦 ) <s ( -us ‘ 𝑥 ) ) ) ) )
58 46 sseli ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 ∈ No )
59 58 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝐿 ∈ No )
60 43 sseli ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) → 𝑥𝑅 ∈ No )
61 60 adantr ⊢ ( ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) → 𝑥𝑅 ∈ No )
62 61 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝑅 ∈ No )
63 39 sseli ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝐴 ) → 𝑥𝐿 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
64 63 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝐿 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
65 oldbdayim ⊢ ( 𝑥𝐿 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑥𝐿 ) ∈ ( bday ‘ 𝐴 ) )
66 64 65 syl ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( bday ‘ 𝑥𝐿 ) ∈ ( bday ‘ 𝐴 ) )
67 12 a1i ⊢ ( 𝜑 → ( R ‘ 𝐴 ) ⊆ ( O ‘ ( bday ‘ 𝐴 ) ) )
68 67 sselda ⊢ ( ( 𝜑 ∧ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ) → 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
69 68 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
70 oldbdayim ⊢ ( 𝑥𝑅 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝑥𝑅 ) ∈ ( bday ‘ 𝐴 ) )
71 69 70 syl ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( bday ‘ 𝑥𝑅 ) ∈ ( bday ‘ 𝐴 ) )
72 bdayelon ⊢ ( bday ‘ 𝑥𝐿 ) ∈ On
73 bdayelon ⊢ ( bday ‘ 𝑥𝑅 ) ∈ On
74 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
75 onunel ⊢ ( ( ( bday ‘ 𝑥𝐿 ) ∈ On ∧ ( bday ‘ 𝑥𝑅 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( ( bday ‘ 𝑥𝐿 ) ∪ ( bday ‘ 𝑥𝑅 ) ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑥𝐿 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑥𝑅 ) ∈ ( bday ‘ 𝐴 ) ) ) )
76 72 73 74 75 mp3an ⊢ ( ( ( bday ‘ 𝑥𝐿 ) ∪ ( bday ‘ 𝑥𝑅 ) ) ∈ ( bday ‘ 𝐴 ) ↔ ( ( bday ‘ 𝑥𝐿 ) ∈ ( bday ‘ 𝐴 ) ∧ ( bday ‘ 𝑥𝑅 ) ∈ ( bday ‘ 𝐴 ) ) )
77 66 71 76 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( ( bday ‘ 𝑥𝐿 ) ∪ ( bday ‘ 𝑥𝑅 ) ) ∈ ( bday ‘ 𝐴 ) )
78 elun1 ⊢ ( ( ( bday ‘ 𝑥𝐿 ) ∪ ( bday ‘ 𝑥𝑅 ) ) ∈ ( bday ‘ 𝐴 ) → ( ( bday ‘ 𝑥𝐿 ) ∪ ( bday ‘ 𝑥𝑅 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
79 77 78 syl ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( ( bday ‘ 𝑥𝐿 ) ∪ ( bday ‘ 𝑥𝑅 ) ) ∈ ( ( bday ‘ 𝐴 ) ∪ ( bday ‘ 𝐵 ) ) )
80 57 59 62 79 negsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝑥𝐿 ) ∈ No ∧ ( 𝑥𝐿 <s 𝑥𝑅 → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥𝐿 ) ) ) )
81 80 simprd ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( 𝑥𝐿 <s 𝑥𝑅 → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥𝐿 ) ) )
82 56 81 mpd ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥𝐿 ) )
83 breq12 ⊢ ( ( ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ( -us ‘ 𝑥𝐿 ) = 𝑏 ) → ( ( -us ‘ 𝑥𝑅 ) <s ( -us ‘ 𝑥𝐿 ) ↔ 𝑎 <s 𝑏 ) )
84 82 83 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ) ) → ( ( ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ( -us ‘ 𝑥𝐿 ) = 𝑏 ) → 𝑎 <s 𝑏 ) )
85 84 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑥𝐿 ∈ ( L ‘ 𝐴 ) ( ( -us ‘ 𝑥𝑅 ) = 𝑎 ∧ ( -us ‘ 𝑥𝐿 ) = 𝑏 ) → 𝑎 <s 𝑏 ) )
86 51 85 biimtrid ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∧ 𝑏 ∈ ( -us “ ( L ‘ 𝐴 ) ) ) → 𝑎 <s 𝑏 ) )
87 86 3impib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( -us “ ( R ‘ 𝐴 ) ) ∧ 𝑏 ∈ ( -us “ ( L ‘ 𝐴 ) ) ) → 𝑎 <s 𝑏 )
88 8 11 38 42 87 ssltd ⊢ ( 𝜑 → ( -us “ ( R ‘ 𝐴 ) ) <<s ( -us “ ( L ‘ 𝐴 ) ) )