Metamath Proof Explorer


Theorem cuteq1

Description: Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025)

Ref Expression
Hypotheses cuteq1.1 φ 0 s A
cuteq1.2 φ A s 1 s
cuteq1.3 φ 1 s s B
Assertion cuteq1 φ A | s B = 1 s

Proof

Step Hyp Ref Expression
1 cuteq1.1 φ 0 s A
2 cuteq1.2 φ A s 1 s
3 cuteq1.3 φ 1 s s B
4 bday1s bday 1 s = 1 𝑜
5 df-1o 1 𝑜 = suc
6 4 5 eqtri bday 1 s = suc
7 ssltsep A s 0 s x A y 0 s x < s y
8 dfral2 y 0 s x < s y ¬ y 0 s ¬ x < s y
9 8 ralbii x A y 0 s x < s y x A ¬ y 0 s ¬ x < s y
10 ralnex x A ¬ y 0 s ¬ x < s y ¬ x A y 0 s ¬ x < s y
11 9 10 bitri x A y 0 s x < s y ¬ x A y 0 s ¬ x < s y
12 7 11 sylib A s 0 s ¬ x A y 0 s ¬ x < s y
13 0sno 0 s No
14 sltirr 0 s No ¬ 0 s < s 0 s
15 13 14 ax-mp ¬ 0 s < s 0 s
16 breq1 x = 0 s x < s 0 s 0 s < s 0 s
17 16 notbid x = 0 s ¬ x < s 0 s ¬ 0 s < s 0 s
18 17 rspcev 0 s A ¬ 0 s < s 0 s x A ¬ x < s 0 s
19 1 15 18 sylancl φ x A ¬ x < s 0 s
20 13 elexi 0 s V
21 breq2 y = 0 s x < s y x < s 0 s
22 21 notbid y = 0 s ¬ x < s y ¬ x < s 0 s
23 20 22 rexsn y 0 s ¬ x < s y ¬ x < s 0 s
24 23 rexbii x A y 0 s ¬ x < s y x A ¬ x < s 0 s
25 19 24 sylibr φ x A y 0 s ¬ x < s y
26 12 25 nsyl3 φ ¬ A s 0 s
27 26 adantr φ x No ¬ A s 0 s
28 sneq x = 0 s x = 0 s
29 28 breq2d x = 0 s A s x A s 0 s
30 29 notbid x = 0 s ¬ A s x ¬ A s 0 s
31 27 30 syl5ibrcom φ x No x = 0 s ¬ A s x
32 31 necon2ad φ x No A s x x 0 s
33 32 adantrd φ x No A s x x s B x 0 s
34 33 impr φ x No A s x x s B x 0 s
35 bday0b x No bday x = x = 0 s
36 35 ad2antrl φ x No A s x x s B bday x = x = 0 s
37 36 necon3bid φ x No A s x x s B bday x x 0 s
38 34 37 mpbird φ x No A s x x s B bday x
39 bdayelon bday x On
40 39 onordi Ord bday x
41 ord0eln0 Ord bday x bday x bday x
42 40 41 ax-mp bday x bday x
43 0elon On
44 43 39 onsucssi bday x suc bday x
45 42 44 bitr3i bday x suc bday x
46 38 45 sylib φ x No A s x x s B suc bday x
47 6 46 eqsstrid φ x No A s x x s B bday 1 s bday x
48 47 expr φ x No A s x x s B bday 1 s bday x
49 48 ralrimiva φ x No A s x x s B bday 1 s bday x
50 1sno 1 s No
51 50 elexi 1 s V
52 51 snnz 1 s
53 sslttr A s 1 s 1 s s B 1 s A s B
54 52 53 mp3an3 A s 1 s 1 s s B A s B
55 2 3 54 syl2anc φ A s B
56 eqscut2 A s B 1 s No A | s B = 1 s A s 1 s 1 s s B x No A s x x s B bday 1 s bday x
57 55 50 56 sylancl φ A | s B = 1 s A s 1 s 1 s s B x No A s x x s B bday 1 s bday x
58 2 3 49 57 mpbir3and φ A | s B = 1 s