Metamath Proof Explorer


Theorem conway

Description: Conway's Simplicity Theorem. Given A preceeding B , there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. Theorem from Alling p. 185. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion conway A s B ∃! x y No | A s y y s B bday x = bday y No | A s y y s B

Proof

Step Hyp Ref Expression
1 ssltss1 A s B A No
2 ssltex1 A s B A V
3 ssltss2 A s B B No
4 ssltex2 A s B B V
5 ssltsep A s B p A q B p < s q
6 noeta2 A No A V B No B V p A q B p < s q y No p A p < s y q B y < s q bday y suc bday A B
7 1 2 3 4 5 6 syl221anc A s B y No p A p < s y q B y < s q bday y suc bday A B
8 3simpa p A p < s y q B y < s q bday y suc bday A B p A p < s y q B y < s q
9 2 ad2antrr A s B y No p A p < s y A V
10 snex y V
11 9 10 jctir A s B y No p A p < s y A V y V
12 1 ad2antrr A s B y No p A p < s y A No
13 snssi y No y No
14 13 adantl A s B y No y No
15 14 adantr A s B y No p A p < s y y No
16 vex y V
17 breq2 q = y p < s q p < s y
18 16 17 ralsn q y p < s q p < s y
19 18 ralbii p A q y p < s q p A p < s y
20 19 biimpri p A p < s y p A q y p < s q
21 20 adantl A s B y No p A p < s y p A q y p < s q
22 12 15 21 3jca A s B y No p A p < s y A No y No p A q y p < s q
23 brsslt A s y A V y V A No y No p A q y p < s q
24 11 22 23 sylanbrc A s B y No p A p < s y A s y
25 24 ex A s B y No p A p < s y A s y
26 4 ad2antrr A s B y No q B y < s q B V
27 26 10 jctil A s B y No q B y < s q y V B V
28 14 adantr A s B y No q B y < s q y No
29 3 ad2antrr A s B y No q B y < s q B No
30 ralcom p y q B p < s q q B p y p < s q
31 breq1 p = y p < s q y < s q
32 16 31 ralsn p y p < s q y < s q
33 32 ralbii q B p y p < s q q B y < s q
34 30 33 sylbbr q B y < s q p y q B p < s q
35 34 adantl A s B y No q B y < s q p y q B p < s q
36 28 29 35 3jca A s B y No q B y < s q y No B No p y q B p < s q
37 brsslt y s B y V B V y No B No p y q B p < s q
38 27 36 37 sylanbrc A s B y No q B y < s q y s B
39 38 ex A s B y No q B y < s q y s B
40 25 39 anim12d A s B y No p A p < s y q B y < s q A s y y s B
41 8 40 syl5 A s B y No p A p < s y q B y < s q bday y suc bday A B A s y y s B
42 41 reximdva A s B y No p A p < s y q B y < s q bday y suc bday A B y No A s y y s B
43 7 42 mpd A s B y No A s y y s B
44 rabn0 y No | A s y y s B y No A s y y s B
45 43 44 sylibr A s B y No | A s y y s B
46 ssrab2 y No | A s y y s B No
47 46 a1i A s B y No | A s y y s B No
48 simplr3 A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No
49 2 ad2antrr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q A V
50 snex r V
51 49 50 jctir A s B p No q No r No A s p p s B A s q q s B p < s r r < s q A V r V
52 1 ad2antrr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q A No
53 snssi r No r No
54 48 53 syl A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No
55 52 sselda A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A x No
56 simplr1 A s B p No q No r No A s p p s B A s q q s B p < s r r < s q p No
57 56 adantr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A p No
58 48 adantr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A r No
59 simplll A s p p s B A s q q s B p < s r r < s q A s p
60 59 adantl A s B p No q No r No A s p p s B A s q q s B p < s r r < s q A s p
61 ssltsep A s p x A y p x < s y
62 60 61 syl A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A y p x < s y
63 62 r19.21bi A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A y p x < s y
64 vex p V
65 breq2 y = p x < s y x < s p
66 64 65 ralsn y p x < s y x < s p
67 63 66 sylib A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A x < s p
68 simprrl A s B p No q No r No A s p p s B A s q q s B p < s r r < s q p < s r
69 68 adantr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A p < s r
70 55 57 58 67 69 slttrd A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A x < s r
71 vex r V
72 breq2 y = r x < s y x < s r
73 71 72 ralsn y r x < s y x < s r
74 70 73 sylibr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A y r x < s y
75 74 ralrimiva A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x A y r x < s y
76 52 54 75 3jca A s B p No q No r No A s p p s B A s q q s B p < s r r < s q A No r No x A y r x < s y
77 brsslt A s r A V r V A No r No x A y r x < s y
78 51 76 77 sylanbrc A s B p No q No r No A s p p s B A s q q s B p < s r r < s q A s r
79 4 ad2antrr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q B V
80 79 50 jctil A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r V B V
81 3 ad2antrr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q B No
82 48 adantr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B r No
83 simplr2 A s B p No q No r No A s p p s B A s q q s B p < s r r < s q q No
84 83 adantr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B q No
85 81 sselda A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B y No
86 simprrr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r < s q
87 86 adantr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B r < s q
88 simplrr A s p p s B A s q q s B p < s r r < s q q s B
89 88 adantl A s B p No q No r No A s p p s B A s q q s B p < s r r < s q q s B
90 ssltsep q s B x q y B x < s y
91 89 90 syl A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x q y B x < s y
92 vex q V
93 breq1 x = q x < s y q < s y
94 93 ralbidv x = q y B x < s y y B q < s y
95 92 94 ralsn x q y B x < s y y B q < s y
96 91 95 sylib A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B q < s y
97 96 r19.21bi A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B q < s y
98 82 84 85 87 97 slttrd A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B r < s y
99 98 ralrimiva A s B p No q No r No A s p p s B A s q q s B p < s r r < s q y B r < s y
100 breq1 x = r x < s y r < s y
101 100 ralbidv x = r y B x < s y y B r < s y
102 71 101 ralsn x r y B x < s y y B r < s y
103 99 102 sylibr A s B p No q No r No A s p p s B A s q q s B p < s r r < s q x r y B x < s y
104 54 81 103 3jca A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No B No x r y B x < s y
105 brsslt r s B r V B V r No B No x r y B x < s y
106 80 104 105 sylanbrc A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r s B
107 48 78 106 jca32 A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B
108 107 exp44 A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B
109 108 ralrimivvva A s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B
110 sneq y = p y = p
111 110 breq2d y = p A s y A s p
112 110 breq1d y = p y s B p s B
113 111 112 anbi12d y = p A s y y s B A s p p s B
114 113 ralrab p y No | A s y y s B q No r No A s q q s B p < s r r < s q r No A s r r s B p No A s p p s B q No r No A s q q s B p < s r r < s q r No A s r r s B
115 sneq y = q y = q
116 115 breq2d y = q A s y A s q
117 115 breq1d y = q y s B q s B
118 116 117 anbi12d y = q A s y y s B A s q q s B
119 118 ralrab q y No | A s y y s B r No p < s r r < s q r No A s r r s B q No A s q q s B r No p < s r r < s q r No A s r r s B
120 sneq y = r y = r
121 120 breq2d y = r A s y A s r
122 120 breq1d y = r y s B r s B
123 121 122 anbi12d y = r A s y y s B A s r r s B
124 123 elrab r y No | A s y y s B r No A s r r s B
125 124 imbi2i p < s r r < s q r y No | A s y y s B p < s r r < s q r No A s r r s B
126 125 ralbii r No p < s r r < s q r y No | A s y y s B r No p < s r r < s q r No A s r r s B
127 126 ralbii q y No | A s y y s B r No p < s r r < s q r y No | A s y y s B q y No | A s y y s B r No p < s r r < s q r No A s r r s B
128 r19.21v r No A s q q s B p < s r r < s q r No A s r r s B A s q q s B r No p < s r r < s q r No A s r r s B
129 128 ralbii q No r No A s q q s B p < s r r < s q r No A s r r s B q No A s q q s B r No p < s r r < s q r No A s r r s B
130 119 127 129 3bitr4i q y No | A s y y s B r No p < s r r < s q r y No | A s y y s B q No r No A s q q s B p < s r r < s q r No A s r r s B
131 130 ralbii p y No | A s y y s B q y No | A s y y s B r No p < s r r < s q r y No | A s y y s B p y No | A s y y s B q No r No A s q q s B p < s r r < s q r No A s r r s B
132 r19.21v r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B A s p p s B r No A s q q s B p < s r r < s q r No A s r r s B
133 132 ralbii q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B q No A s p p s B r No A s q q s B p < s r r < s q r No A s r r s B
134 r19.21v q No A s p p s B r No A s q q s B p < s r r < s q r No A s r r s B A s p p s B q No r No A s q q s B p < s r r < s q r No A s r r s B
135 133 134 bitri q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B A s p p s B q No r No A s q q s B p < s r r < s q r No A s r r s B
136 135 ralbii p No q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B p No A s p p s B q No r No A s q q s B p < s r r < s q r No A s r r s B
137 114 131 136 3bitr4i p y No | A s y y s B q y No | A s y y s B r No p < s r r < s q r y No | A s y y s B p No q No r No A s p p s B A s q q s B p < s r r < s q r No A s r r s B
138 109 137 sylibr A s B p y No | A s y y s B q y No | A s y y s B r No p < s r r < s q r y No | A s y y s B
139 nocvxmin y No | A s y y s B y No | A s y y s B No p y No | A s y y s B q y No | A s y y s B r No p < s r r < s q r y No | A s y y s B ∃! x y No | A s y y s B bday x = bday y No | A s y y s B
140 45 47 138 139 syl3anc A s B ∃! x y No | A s y y s B bday x = bday y No | A s y y s B