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 < E! x e. { y e. No | ( A <

Proof

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