Metamath Proof Explorer

Theorem eqscut3

Description: A variant of the simplicity theorem - if B lies between the cut sets of A but none of its options do, then A = B . Theorem 11 of Conway p. 23. (Contributed by Scott Fenton, 28-Nov-2025)

Ref Expression
Hypotheses eqscut3.1 
|- ( ph -> L <
eqscut3.2 
|- ( ph -> M <
eqscut3.3 
|- ( ph -> A = ( L |s R ) )
eqscut3.4 
|- ( ph -> B = ( M |s S ) )
eqscut3.5 
|- ( ph -> L <
eqscut3.6 
|- ( ph -> { B } <
eqscut3.7 
|- ( ph -> A. xO e. ( M u. S ) -. ( L <
Assertion eqscut3 
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 eqscut3.1 
 |-  ( ph -> L <
2 eqscut3.2 
 |-  ( ph -> M <
3 eqscut3.3 
 |-  ( ph -> A = ( L |s R ) )
4 eqscut3.4 
 |-  ( ph -> B = ( M |s S ) )
5 eqscut3.5 
 |-  ( ph -> L <
6 eqscut3.6 
 |-  ( ph -> { B } <
7 eqscut3.7 
 |-  ( ph -> A. xO e. ( M u. S ) -. ( L <
8 sneq 
 |-  ( xO = zR -> { xO } = { zR } )
9 8 breq2d 
 |-  ( xO = zR -> ( L < L <
10 8 breq1d 
 |-  ( xO = zR -> ( { xO } < { zR } <
11 9 10 anbi12d 
 |-  ( xO = zR -> ( ( L < ( L <
12 11 notbid 
 |-  ( xO = zR -> ( -. ( L < -. ( L <
13 7 adantr 
 |-  ( ( ph /\ zR e. S ) -> A. xO e. ( M u. S ) -. ( L <
14 elun2 
 |-  ( zR e. S -> zR e. ( M u. S ) )
15 14 adantl 
 |-  ( ( ph /\ zR e. S ) -> zR e. ( M u. S ) )
16 12 13 15 rspcdva 
 |-  ( ( ph /\ zR e. S ) -> -. ( L <
17 5 ad2antrr 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> L <
18 4 sneqd 
 |-  ( ph -> { B } = { ( M |s S ) } )
19 scutcut 
 |-  ( M < ( ( M |s S ) e. No /\ M <
20 2 19 syl 
 |-  ( ph -> ( ( M |s S ) e. No /\ M <
21 20 simp3d 
 |-  ( ph -> { ( M |s S ) } <
22 18 21 eqbrtrd 
 |-  ( ph -> { B } <
23 22 ad2antrr 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } <
24 simplr 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> zR e. S )
25 24 snssd 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } C_ S )
26 sssslt2 
 |-  ( ( { B } < { B } <
27 23 25 26 syl2anc 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } <
28 2 scutcld 
 |-  ( ph -> ( M |s S ) e. No )
29 4 28 eqeltrd 
 |-  ( ph -> B e. No )
30 snnzg 
 |-  ( B e. No -> { B } =/= (/) )
31 29 30 syl 
 |-  ( ph -> { B } =/= (/) )
32 31 ad2antrr 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { B } =/= (/) )
33 sslttr 
 |-  ( ( L < L <
34 17 27 32 33 syl3anc 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> L <
35 snex 
 |-  { zR } e. _V
36 35 a1i 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } e. _V )
37 ssltex2 
 |-  ( L < R e. _V )
38 1 37 syl 
 |-  ( ph -> R e. _V )
39 38 ad2antrr 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> R e. _V )
40 ssltss2 
 |-  ( { B } < { zR } C_ No )
41 27 40 syl 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } C_ No )
42 ssltss2 
 |-  ( L < R C_ No )
43 1 42 syl 
 |-  ( ph -> R C_ No )
44 43 ad2antrr 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> R C_ No )
45 simpll 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ( ph /\ zR e. S ) )
46 ssltss2 
 |-  ( M < S C_ No )
47 2 46 syl 
 |-  ( ph -> S C_ No )
48 47 sselda 
 |-  ( ( ph /\ zR e. S ) -> zR e. No )
49 45 48 syl 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR e. No )
50 simplll 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ph )
51 1 scutcld 
 |-  ( ph -> ( L |s R ) e. No )
52 3 51 eqeltrd 
 |-  ( ph -> A e. No )
53 50 52 syl 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A e. No )
54 44 sselda 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> xR e. No )
55 simplr 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR <_s A )
56 scutcut 
 |-  ( L < ( ( L |s R ) e. No /\ L <
57 1 56 syl 
 |-  ( ph -> ( ( L |s R ) e. No /\ L <
58 57 simp3d 
 |-  ( ph -> { ( L |s R ) } <
59 58 adantr 
 |-  ( ( ph /\ zR e. S ) -> { ( L |s R ) } <
60 59 ad2antrr 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> { ( L |s R ) } <
61 ovex 
 |-  ( L |s R ) e. _V
62 61 elsn2 
 |-  ( A e. { ( L |s R ) } <-> A = ( L |s R ) )
63 3 62 sylibr 
 |-  ( ph -> A e. { ( L |s R ) } )
64 63 adantr 
 |-  ( ( ph /\ zR e. S ) -> A e. { ( L |s R ) } )
65 64 ad2antrr 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A e. { ( L |s R ) } )
66 simpr 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> xR e. R )
67 60 65 66 ssltsepcd 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> A
68 49 53 54 55 67 slelttrd 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> zR
69 velsn 
 |-  ( x e. { zR } <-> x = zR )
70 breq1 
 |-  ( x = zR -> ( x  zR
71 69 70 sylbi 
 |-  ( x e. { zR } -> ( x  zR
72 68 71 syl5ibrcom 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ xR e. R ) -> ( x e. { zR } -> x
73 72 ex 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> ( xR e. R -> ( x e. { zR } -> x
74 73 com23 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> ( x e. { zR } -> ( xR e. R -> x
75 74 3imp 
 |-  ( ( ( ( ph /\ zR e. S ) /\ zR <_s A ) /\ x e. { zR } /\ xR e. R ) -> x
76 36 39 41 44 75 ssltd 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> { zR } <
77 34 76 jca 
 |-  ( ( ( ph /\ zR e. S ) /\ zR <_s A ) -> ( L <
78 16 77 mtand 
 |-  ( ( ph /\ zR e. S ) -> -. zR <_s A )
79 52 adantr 
 |-  ( ( ph /\ zR e. S ) -> A e. No )
80 sltnle 
 |-  ( ( A e. No /\ zR e. No ) -> ( A  -. zR <_s A ) )
81 79 48 80 syl2anc 
 |-  ( ( ph /\ zR e. S ) -> ( A  -. zR <_s A ) )
82 78 81 mpbird 
 |-  ( ( ph /\ zR e. S ) -> A
83 82 ralrimiva 
 |-  ( ph -> A. zR e. S A
84 ssltsep 
 |-  ( L < A. x e. L A. y e. { B } x
85 5 84 syl 
 |-  ( ph -> A. x e. L A. y e. { B } x
86 breq2 
 |-  ( y = B -> ( x  x
87 86 ralsng 
 |-  ( B e. No -> ( A. y e. { B } x  x
88 29 87 syl 
 |-  ( ph -> ( A. y e. { B } x  x
89 88 ralbidv 
 |-  ( ph -> ( A. x e. L A. y e. { B } x  A. x e. L x
90 85 89 mpbid 
 |-  ( ph -> A. x e. L x
91 1 2 3 4 slerecd 
 |-  ( ph -> ( A <_s B <-> ( A. zR e. S A
92 83 90 91 mpbir2and 
 |-  ( ph -> A <_s B )
93 ssltsep 
 |-  ( { B } < A. x e. { B } A. y e. R x
94 6 93 syl 
 |-  ( ph -> A. x e. { B } A. y e. R x
95 breq1 
 |-  ( x = B -> ( x  B
96 95 ralbidv 
 |-  ( x = B -> ( A. y e. R x  A. y e. R B
97 96 ralsng 
 |-  ( B e. No -> ( A. x e. { B } A. y e. R x  A. y e. R B
98 29 97 syl 
 |-  ( ph -> ( A. x e. { B } A. y e. R x  A. y e. R B
99 94 98 mpbid 
 |-  ( ph -> A. y e. R B
100 sneq 
 |-  ( xO = zL -> { xO } = { zL } )
101 100 breq2d 
 |-  ( xO = zL -> ( L < L <
102 100 breq1d 
 |-  ( xO = zL -> ( { xO } < { zL } <
103 101 102 anbi12d 
 |-  ( xO = zL -> ( ( L < ( L <
104 103 notbid 
 |-  ( xO = zL -> ( -. ( L < -. ( L <
105 7 adantr 
 |-  ( ( ph /\ zL e. M ) -> A. xO e. ( M u. S ) -. ( L <
106 elun1 
 |-  ( zL e. M -> zL e. ( M u. S ) )
107 106 adantl 
 |-  ( ( ph /\ zL e. M ) -> zL e. ( M u. S ) )
108 104 105 107 rspcdva 
 |-  ( ( ph /\ zL e. M ) -> -. ( L <
109 ssltex1 
 |-  ( L < L e. _V )
110 1 109 syl 
 |-  ( ph -> L e. _V )
111 110 ad2antrr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L e. _V )
112 snex 
 |-  { zL } e. _V
113 112 a1i 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } e. _V )
114 ssltss1 
 |-  ( L < L C_ No )
115 1 114 syl 
 |-  ( ph -> L C_ No )
116 115 adantr 
 |-  ( ( ph /\ zL e. M ) -> L C_ No )
117 116 adantr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L C_ No )
118 simplr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> zL e. M )
119 118 snssd 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } C_ M )
120 ssltss1 
 |-  ( M < M C_ No )
121 2 120 syl 
 |-  ( ph -> M C_ No )
122 121 ad2antrr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> M C_ No )
123 119 122 sstrd 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } C_ No )
124 117 sselda 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL e. No )
125 simplll 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> ph )
126 125 52 syl 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A e. No )
127 121 sselda 
 |-  ( ( ph /\ zL e. M ) -> zL e. No )
128 127 adantr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> zL e. No )
129 128 adantr 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> zL e. No )
130 57 simp2d 
 |-  ( ph -> L <
131 130 adantr 
 |-  ( ( ph /\ zL e. M ) -> L <
132 131 adantr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L <
133 132 adantr 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> L <
134 simpr 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL e. L )
135 63 adantr 
 |-  ( ( ph /\ zL e. M ) -> A e. { ( L |s R ) } )
136 135 adantr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> A e. { ( L |s R ) } )
137 136 adantr 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A e. { ( L |s R ) } )
138 133 134 137 ssltsepcd 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL
139 simplr 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> A <_s zL )
140 124 126 129 138 139 sltletrd 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> xL
141 velsn 
 |-  ( x e. { zL } <-> x = zL )
142 breq2 
 |-  ( x = zL -> ( xL  xL
143 141 142 sylbi 
 |-  ( x e. { zL } -> ( xL  xL
144 140 143 syl5ibrcom 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L ) -> ( x e. { zL } -> xL
145 144 3impia 
 |-  ( ( ( ( ph /\ zL e. M ) /\ A <_s zL ) /\ xL e. L /\ x e. { zL } ) -> xL
146 111 113 117 123 145 ssltd 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> L <
147 20 simp2d 
 |-  ( ph -> M <
148 147 18 breqtrrd 
 |-  ( ph -> M <
149 148 adantr 
 |-  ( ( ph /\ zL e. M ) -> M <
150 149 adantr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> M <
151 sssslt1 
 |-  ( ( M < { zL } <
152 150 119 151 syl2anc 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } <
153 simpll 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> ph )
154 153 6 syl 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { B } <
155 31 adantr 
 |-  ( ( ph /\ zL e. M ) -> { B } =/= (/) )
156 155 adantr 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { B } =/= (/) )
157 sslttr 
 |-  ( ( { zL } < { zL } <
158 152 154 156 157 syl3anc 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> { zL } <
159 146 158 jca 
 |-  ( ( ( ph /\ zL e. M ) /\ A <_s zL ) -> ( L <
160 108 159 mtand 
 |-  ( ( ph /\ zL e. M ) -> -. A <_s zL )
161 52 adantr 
 |-  ( ( ph /\ zL e. M ) -> A e. No )
162 sltnle 
 |-  ( ( zL e. No /\ A e. No ) -> ( zL  -. A <_s zL ) )
163 127 161 162 syl2anc 
 |-  ( ( ph /\ zL e. M ) -> ( zL  -. A <_s zL ) )
164 160 163 mpbird 
 |-  ( ( ph /\ zL e. M ) -> zL
165 164 ralrimiva 
 |-  ( ph -> A. zL e. M zL
166 2 1 4 3 slerecd 
 |-  ( ph -> ( B <_s A <-> ( A. y e. R B
167 99 165 166 mpbir2and 
 |-  ( ph -> B <_s A )
168 sletri3 
 |-  ( ( A e. No /\ B e. No ) -> ( A = B <-> ( A <_s B /\ B <_s A ) ) )
169 52 29 168 syl2anc 
 |-  ( ph -> ( A = B <-> ( A <_s B /\ B <_s A ) ) )
170 92 167 169 mpbir2and 
 |-  ( ph -> A = B )