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