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 sltsss1 
 |-  ( A < A C_ No )
2 sltsex1 
 |-  ( A < A e. _V )
3 sltsss2 
 |-  ( A < B C_ No )
4 sltsex2 
 |-  ( A < B e. _V )
5 sltssep 
 |-  ( 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 vsnex 
 |-  { 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 brslts 
 |-  ( 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 brslts 
 |-  ( { 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 vsnex 
 |-  { r } e. _V
51 49 50 jctir 
 |-  ( ( ( A < ( A e. _V /\ { r } e. _V ) )
52 1 ad2antrr 
 |-  ( ( ( A < A C_ No )
53 48 snssd 
 |-  ( ( ( A < { r } C_ No )
54 52 sselda 
 |-  ( ( ( ( A < x e. No )
55 simplr1 
 |-  ( ( ( A < p e. No )
56 55 adantr 
 |-  ( ( ( ( A < p e. No )
57 48 adantr 
 |-  ( ( ( ( A < r e. No )
58 simplll 
 |-  ( ( ( ( A < A <
59 58 adantl 
 |-  ( ( ( A < A <
60 sltssep 
 |-  ( A < A. x e. A A. y e. { p } x
61 59 60 syl 
 |-  ( ( ( A < A. x e. A A. y e. { p } x
62 61 r19.21bi 
 |-  ( ( ( ( A < A. y e. { p } x
63 vex 
 |-  p e. _V
64 breq2 
 |-  ( y = p -> ( x  x
65 63 64 ralsn 
 |-  ( A. y e. { p } x  x
66 62 65 sylib 
 |-  ( ( ( ( A < x
67 simprrl 
 |-  ( ( ( A < p
68 67 adantr 
 |-  ( ( ( ( A < p
69 54 56 57 66 68 ltstrd 
 |-  ( ( ( ( A < x
70 vex 
 |-  r e. _V
71 breq2 
 |-  ( y = r -> ( x  x
72 70 71 ralsn 
 |-  ( A. y e. { r } x  x
73 69 72 sylibr 
 |-  ( ( ( ( A < A. y e. { r } x
74 73 ralrimiva 
 |-  ( ( ( A < A. x e. A A. y e. { r } x
75 52 53 74 3jca 
 |-  ( ( ( A < ( A C_ No /\ { r } C_ No /\ A. x e. A A. y e. { r } x
76 brslts 
 |-  ( A < ( ( A e. _V /\ { r } e. _V ) /\ ( A C_ No /\ { r } C_ No /\ A. x e. A A. y e. { r } x
77 51 75 76 sylanbrc 
 |-  ( ( ( A < A <
78 4 ad2antrr 
 |-  ( ( ( A < B e. _V )
79 78 50 jctil 
 |-  ( ( ( A < ( { r } e. _V /\ B e. _V ) )
80 3 ad2antrr 
 |-  ( ( ( A < B C_ No )
81 48 adantr 
 |-  ( ( ( ( A < r e. No )
82 simplr2 
 |-  ( ( ( A < q e. No )
83 82 adantr 
 |-  ( ( ( ( A < q e. No )
84 80 sselda 
 |-  ( ( ( ( A < y e. No )
85 simprrr 
 |-  ( ( ( A < r
86 85 adantr 
 |-  ( ( ( ( A < r
87 simplrr 
 |-  ( ( ( ( A < { q } <
88 87 adantl 
 |-  ( ( ( A < { q } <
89 sltssep 
 |-  ( { q } < A. x e. { q } A. y e. B x
90 88 89 syl 
 |-  ( ( ( A < A. x e. { q } A. y e. B x
91 vex 
 |-  q e. _V
92 breq1 
 |-  ( x = q -> ( x  q
93 92 ralbidv 
 |-  ( x = q -> ( A. y e. B x  A. y e. B q
94 91 93 ralsn 
 |-  ( A. x e. { q } A. y e. B x  A. y e. B q
95 90 94 sylib 
 |-  ( ( ( A < A. y e. B q
96 95 r19.21bi 
 |-  ( ( ( ( A < q
97 81 83 84 86 96 ltstrd 
 |-  ( ( ( ( A < r
98 97 ralrimiva 
 |-  ( ( ( A < A. y e. B r
99 breq1 
 |-  ( x = r -> ( x  r
100 99 ralbidv 
 |-  ( x = r -> ( A. y e. B x  A. y e. B r
101 70 100 ralsn 
 |-  ( A. x e. { r } A. y e. B x  A. y e. B r
102 98 101 sylibr 
 |-  ( ( ( A < A. x e. { r } A. y e. B x
103 53 80 102 3jca 
 |-  ( ( ( A < ( { r } C_ No /\ B C_ No /\ A. x e. { r } A. y e. B x
104 brslts 
 |-  ( { r } < ( ( { r } e. _V /\ B e. _V ) /\ ( { r } C_ No /\ B C_ No /\ A. x e. { r } A. y e. B x
105 79 103 104 sylanbrc 
 |-  ( ( ( A < { r } <
106 48 77 105 jca32 
 |-  ( ( ( A < ( r e. No /\ ( A <
107 106 exp44 
 |-  ( ( A < ( ( A < ( ( A < ( ( p  ( r e. No /\ ( A <
108 107 ralrimivvva 
 |-  ( A < A. p e. No A. q e. No A. r e. No ( ( A < ( ( A < ( ( p  ( r e. No /\ ( A <
109 sneq 
 |-  ( y = p -> { y } = { p } )
110 109 breq2d 
 |-  ( y = p -> ( A < A <
111 109 breq1d 
 |-  ( y = p -> ( { y } < { p } <
112 110 111 anbi12d 
 |-  ( y = p -> ( ( A < ( A <
113 112 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 <
114 sneq 
 |-  ( y = q -> { y } = { q } )
115 114 breq2d 
 |-  ( y = q -> ( A < A <
116 114 breq1d 
 |-  ( y = q -> ( { y } < { q } <
117 115 116 anbi12d 
 |-  ( y = q -> ( ( A < ( A <
118 117 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 <
119 sneq 
 |-  ( y = r -> { y } = { r } )
120 119 breq2d 
 |-  ( y = r -> ( A < A <
121 119 breq1d 
 |-  ( y = r -> ( { y } < { r } <
122 120 121 anbi12d 
 |-  ( y = r -> ( ( A < ( A <
123 122 elrab 
 |-  ( r e. { y e. No | ( A < ( r e. No /\ ( A <
124 123 imbi2i 
 |-  ( ( ( p  r e. { y e. No | ( A < ( ( p  ( r e. No /\ ( A <
125 124 ralbii 
 |-  ( A. r e. No ( ( p  r e. { y e. No | ( A < A. r e. No ( ( p  ( r e. No /\ ( A <
126 125 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 <
127 r19.21v 
 |-  ( A. r e. No ( ( A < ( ( p  ( r e. No /\ ( A < ( ( A < A. r e. No ( ( p  ( r e. No /\ ( A <
128 127 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 <
129 118 126 128 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 <
130 129 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 <
131 r19.21v 
 |-  ( A. r e. No ( ( A < ( ( A < ( ( p  ( r e. No /\ ( A < ( ( A < A. r e. No ( ( A < ( ( p  ( r e. No /\ ( A <
132 131 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 <
133 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 <
134 132 133 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 <
135 134 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 <
136 113 130 135 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 <
137 108 136 sylibr 
 |-  ( A < A. p e. { y e. No | ( A < r e. { y e. No | ( A <
138 nocvxmin 
 |-  ( ( { y e. No | ( A < r e. { y e. No | ( A < E! x e. { y e. No | ( A <
139 45 47 137 138 syl3anc 
 |-  ( A < E! x e. { y e. No | ( A <