Metamath Proof Explorer

Theorem cofcutr

Description: If X is the cut of A and B , then A is cofinal with (LeftX ) and B is coinitial with ( RightX ) . Theorem 2.9 of Gonshor p. 12. (Contributed by Scott Fenton, 25-Sep-2024)

Ref Expression
Assertion cofcutr 
|- ( ( A < ( A. x e. ( _Left ` X ) E. y e. A x <_s y /\ A. z e. ( _Right ` X ) E. w e. B w <_s z ) )

Proof

Step Hyp Ref Expression
1 bdayelon 
 |-  ( bday ` ( A |s B ) ) e. On
2 1 onssneli 
 |-  ( ( bday ` ( A |s B ) ) C_ ( bday ` x ) -> -. ( bday ` x ) e. ( bday ` ( A |s B ) ) )
3 leftssold 
 |-  ( _Left ` X ) C_ ( _Old ` ( bday ` X ) )
4 3 a1i 
 |-  ( ( A < ( _Left ` X ) C_ ( _Old ` ( bday ` X ) ) )
5 4 sselda 
 |-  ( ( ( A < x e. ( _Old ` ( bday ` X ) ) )
6 bdayelon 
 |-  ( bday ` X ) e. On
7 leftssno 
 |-  ( _Left ` X ) C_ No
8 7 a1i 
 |-  ( ( A < ( _Left ` X ) C_ No )
9 8 sselda 
 |-  ( ( ( A < x e. No )
10 oldbday 
 |-  ( ( ( bday ` X ) e. On /\ x e. No ) -> ( x e. ( _Old ` ( bday ` X ) ) <-> ( bday ` x ) e. ( bday ` X ) ) )
11 6 9 10 sylancr 
 |-  ( ( ( A < ( x e. ( _Old ` ( bday ` X ) ) <-> ( bday ` x ) e. ( bday ` X ) ) )
12 5 11 mpbid 
 |-  ( ( ( A < ( bday ` x ) e. ( bday ` X ) )
13 simplr 
 |-  ( ( ( A < X = ( A |s B ) )
14 13 fveq2d 
 |-  ( ( ( A < ( bday ` X ) = ( bday ` ( A |s B ) ) )
15 12 14 eleqtrd 
 |-  ( ( ( A < ( bday ` x ) e. ( bday ` ( A |s B ) ) )
16 2 15 nsyl3 
 |-  ( ( ( A < -. ( bday ` ( A |s B ) ) C_ ( bday ` x ) )
17 scutbday 
 |-  ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
18 17 ad3antrrr 
 |-  ( ( ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
19 bdayfn 
 |-  bday Fn No
20 ssrab2 
 |-  { t e. No | ( A <
21 sneq 
 |-  ( t = x -> { t } = { x } )
22 21 breq2d 
 |-  ( t = x -> ( A < A <
23 21 breq1d 
 |-  ( t = x -> ( { t } < { x } <
24 22 23 anbi12d 
 |-  ( t = x -> ( ( A < ( A <
25 9 adantr 
 |-  ( ( ( ( A < x e. No )
26 vsnex 
 |-  { x } e. _V
27 26 a1i 
 |-  ( ( ( A < { x } e. _V )
28 ssltex2 
 |-  ( A < B e. _V )
29 28 ad2antrr 
 |-  ( ( ( A < B e. _V )
30 9 snssd 
 |-  ( ( ( A < { x } C_ No )
31 ssltss2 
 |-  ( A < B C_ No )
32 31 ad2antrr 
 |-  ( ( ( A < B C_ No )
33 9 adantr 
 |-  ( ( ( ( A < x e. No )
34 simpr 
 |-  ( ( A < X = ( A |s B ) )
35 simpl 
 |-  ( ( A < A <
36 35 scutcld 
 |-  ( ( A < ( A |s B ) e. No )
37 34 36 eqeltrd 
 |-  ( ( A < X e. No )
38 37 ad2antrr 
 |-  ( ( ( ( A < X e. No )
39 32 sselda 
 |-  ( ( ( ( A < b e. No )
40 leftval 
 |-  ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
41 40 a1i 
 |-  ( ( A < ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
42 41 eleq2d 
 |-  ( ( A < ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
43 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` X ) ) | x  ( x e. ( _Old ` ( bday ` X ) ) /\ x
44 42 43 bitrdi 
 |-  ( ( A < ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
45 44 simplbda 
 |-  ( ( ( A < x
46 45 adantr 
 |-  ( ( ( ( A < x
47 simpllr 
 |-  ( ( ( ( A < X = ( A |s B ) )
48 scutcut 
 |-  ( A < ( ( A |s B ) e. No /\ A <
49 48 ad2antrr 
 |-  ( ( ( A < ( ( A |s B ) e. No /\ A <
50 49 simp3d 
 |-  ( ( ( A < { ( A |s B ) } <
51 ovex 
 |-  ( A |s B ) e. _V
52 51 snid 
 |-  ( A |s B ) e. { ( A |s B ) }
53 ssltsepc 
 |-  ( ( { ( A |s B ) } < ( A |s B )
54 52 53 mp3an2 
 |-  ( ( { ( A |s B ) } < ( A |s B )
55 50 54 sylan 
 |-  ( ( ( ( A < ( A |s B )
56 47 55 eqbrtrd 
 |-  ( ( ( ( A < X
57 33 38 39 46 56 slttrd 
 |-  ( ( ( ( A < x
58 57 3adant2 
 |-  ( ( ( ( A < x
59 velsn 
 |-  ( a e. { x } <-> a = x )
60 breq1 
 |-  ( a = x -> ( a  x
61 59 60 sylbi 
 |-  ( a e. { x } -> ( a  x
62 61 3ad2ant2 
 |-  ( ( ( ( A < ( a  x
63 58 62 mpbird 
 |-  ( ( ( ( A < a
64 27 29 30 32 63 ssltd 
 |-  ( ( ( A < { x } <
65 64 anim1ci 
 |-  ( ( ( ( A < ( A <
66 24 25 65 elrabd 
 |-  ( ( ( ( A < x e. { t e. No | ( A <
67 fnfvima 
 |-  ( ( bday Fn No /\ { t e. No | ( A < ( bday ` x ) e. ( bday " { t e. No | ( A <
68 19 20 66 67 mp3an12i 
 |-  ( ( ( ( A < ( bday ` x ) e. ( bday " { t e. No | ( A <
69 intss1 
 |-  ( ( bday ` x ) e. ( bday " { t e. No | ( A < |^| ( bday " { t e. No | ( A <
70 68 69 syl 
 |-  ( ( ( ( A < |^| ( bday " { t e. No | ( A <
71 18 70 eqsstrd 
 |-  ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` x ) )
72 16 71 mtand 
 |-  ( ( ( A < -. A <
73 ssltex1 
 |-  ( A < A e. _V )
74 73 ad3antrrr 
 |-  ( ( ( ( A < A e. _V )
75 74 26 jctir 
 |-  ( ( ( ( A < ( A e. _V /\ { x } e. _V ) )
76 ssltss1 
 |-  ( A < A C_ No )
77 76 ad3antrrr 
 |-  ( ( ( ( A < A C_ No )
78 9 adantr 
 |-  ( ( ( ( A < x e. No )
79 78 snssd 
 |-  ( ( ( ( A < { x } C_ No )
80 simpr 
 |-  ( ( ( ( A < A. y e. A A. t e. { x } y
81 77 79 80 3jca 
 |-  ( ( ( ( A < ( A C_ No /\ { x } C_ No /\ A. y e. A A. t e. { x } y
82 brsslt 
 |-  ( A < ( ( A e. _V /\ { x } e. _V ) /\ ( A C_ No /\ { x } C_ No /\ A. y e. A A. t e. { x } y
83 75 81 82 sylanbrc 
 |-  ( ( ( ( A < A <
84 72 83 mtand 
 |-  ( ( ( A < -. A. y e. A A. t e. { x } y
85 rexnal 
 |-  ( E. t e. { x } -. A. y e. A y  -. A. t e. { x } A. y e. A y
86 ralcom 
 |-  ( A. t e. { x } A. y e. A y  A. y e. A A. t e. { x } y
87 85 86 xchbinx 
 |-  ( E. t e. { x } -. A. y e. A y  -. A. y e. A A. t e. { x } y
88 84 87 sylibr 
 |-  ( ( ( A < E. t e. { x } -. A. y e. A y
89 vex 
 |-  x e. _V
90 breq2 
 |-  ( t = x -> ( y  y
91 90 ralbidv 
 |-  ( t = x -> ( A. y e. A y  A. y e. A y
92 91 notbid 
 |-  ( t = x -> ( -. A. y e. A y  -. A. y e. A y
93 89 92 rexsn 
 |-  ( E. t e. { x } -. A. y e. A y  -. A. y e. A y
94 88 93 sylib 
 |-  ( ( ( A < -. A. y e. A y
95 76 ad2antrr 
 |-  ( ( ( A < A C_ No )
96 95 sselda 
 |-  ( ( ( ( A < y e. No )
97 slenlt 
 |-  ( ( x e. No /\ y e. No ) -> ( x <_s y <-> -. y
98 9 96 97 syl2an2r 
 |-  ( ( ( ( A < ( x <_s y <-> -. y
99 98 rexbidva 
 |-  ( ( ( A < ( E. y e. A x <_s y <-> E. y e. A -. y
100 rexnal 
 |-  ( E. y e. A -. y  -. A. y e. A y
101 99 100 bitrdi 
 |-  ( ( ( A < ( E. y e. A x <_s y <-> -. A. y e. A y
102 94 101 mpbird 
 |-  ( ( ( A < E. y e. A x <_s y )
103 102 ralrimiva 
 |-  ( ( A < A. x e. ( _Left ` X ) E. y e. A x <_s y )
104 1 onssneli 
 |-  ( ( bday ` ( A |s B ) ) C_ ( bday ` z ) -> -. ( bday ` z ) e. ( bday ` ( A |s B ) ) )
105 rightssold 
 |-  ( _Right ` X ) C_ ( _Old ` ( bday ` X ) )
106 105 a1i 
 |-  ( ( A < ( _Right ` X ) C_ ( _Old ` ( bday ` X ) ) )
107 106 sselda 
 |-  ( ( ( A < z e. ( _Old ` ( bday ` X ) ) )
108 rightssno 
 |-  ( _Right ` X ) C_ No
109 108 a1i 
 |-  ( ( A < ( _Right ` X ) C_ No )
110 109 sselda 
 |-  ( ( ( A < z e. No )
111 oldbday 
 |-  ( ( ( bday ` X ) e. On /\ z e. No ) -> ( z e. ( _Old ` ( bday ` X ) ) <-> ( bday ` z ) e. ( bday ` X ) ) )
112 6 110 111 sylancr 
 |-  ( ( ( A < ( z e. ( _Old ` ( bday ` X ) ) <-> ( bday ` z ) e. ( bday ` X ) ) )
113 107 112 mpbid 
 |-  ( ( ( A < ( bday ` z ) e. ( bday ` X ) )
114 simplr 
 |-  ( ( ( A < X = ( A |s B ) )
115 114 fveq2d 
 |-  ( ( ( A < ( bday ` X ) = ( bday ` ( A |s B ) ) )
116 113 115 eleqtrd 
 |-  ( ( ( A < ( bday ` z ) e. ( bday ` ( A |s B ) ) )
117 104 116 nsyl3 
 |-  ( ( ( A < -. ( bday ` ( A |s B ) ) C_ ( bday ` z ) )
118 17 ad3antrrr 
 |-  ( ( ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
119 sneq 
 |-  ( t = z -> { t } = { z } )
120 119 breq2d 
 |-  ( t = z -> ( A < A <
121 119 breq1d 
 |-  ( t = z -> ( { t } < { z } <
122 120 121 anbi12d 
 |-  ( t = z -> ( ( A < ( A <
123 110 adantr 
 |-  ( ( ( ( A < z e. No )
124 73 ad2antrr 
 |-  ( ( ( A < A e. _V )
125 vsnex 
 |-  { z } e. _V
126 125 a1i 
 |-  ( ( ( A < { z } e. _V )
127 76 ad2antrr 
 |-  ( ( ( A < A C_ No )
128 110 snssd 
 |-  ( ( ( A < { z } C_ No )
129 127 sselda 
 |-  ( ( ( ( A < a e. No )
130 37 ad2antrr 
 |-  ( ( ( ( A < X e. No )
131 110 adantr 
 |-  ( ( ( ( A < z e. No )
132 48 ad2antrr 
 |-  ( ( ( A < ( ( A |s B ) e. No /\ A <
133 132 simp2d 
 |-  ( ( ( A < A <
134 ssltsepc 
 |-  ( ( A < a
135 52 134 mp3an3 
 |-  ( ( A < a
136 133 135 sylan 
 |-  ( ( ( ( A < a
137 simpllr 
 |-  ( ( ( ( A < X = ( A |s B ) )
138 136 137 breqtrrd 
 |-  ( ( ( ( A < a
139 rightval 
 |-  ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
140 139 a1i 
 |-  ( ( A < ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
141 140 eleq2d 
 |-  ( ( A < ( z e. ( _Right ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X
142 rabid 
 |-  ( z e. { z e. ( _Old ` ( bday ` X ) ) | X  ( z e. ( _Old ` ( bday ` X ) ) /\ X
143 141 142 bitrdi 
 |-  ( ( A < ( z e. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X
144 143 simplbda 
 |-  ( ( ( A < X
145 144 adantr 
 |-  ( ( ( ( A < X
146 129 130 131 138 145 slttrd 
 |-  ( ( ( ( A < a
147 146 3adant3 
 |-  ( ( ( ( A < a
148 velsn 
 |-  ( b e. { z } <-> b = z )
149 breq2 
 |-  ( b = z -> ( a  a
150 148 149 sylbi 
 |-  ( b e. { z } -> ( a  a
151 150 3ad2ant3 
 |-  ( ( ( ( A < ( a  a
152 147 151 mpbird 
 |-  ( ( ( ( A < a
153 124 126 127 128 152 ssltd 
 |-  ( ( ( A < A <
154 153 anim1i 
 |-  ( ( ( ( A < ( A <
155 122 123 154 elrabd 
 |-  ( ( ( ( A < z e. { t e. No | ( A <
156 fnfvima 
 |-  ( ( bday Fn No /\ { t e. No | ( A < ( bday ` z ) e. ( bday " { t e. No | ( A <
157 19 20 155 156 mp3an12i 
 |-  ( ( ( ( A < ( bday ` z ) e. ( bday " { t e. No | ( A <
158 intss1 
 |-  ( ( bday ` z ) e. ( bday " { t e. No | ( A < |^| ( bday " { t e. No | ( A <
159 157 158 syl 
 |-  ( ( ( ( A < |^| ( bday " { t e. No | ( A <
160 118 159 eqsstrd 
 |-  ( ( ( ( A < ( bday ` ( A |s B ) ) C_ ( bday ` z ) )
161 117 160 mtand 
 |-  ( ( ( A < -. { z } <
162 28 ad3antrrr 
 |-  ( ( ( ( A < B e. _V )
163 162 125 jctil 
 |-  ( ( ( ( A < ( { z } e. _V /\ B e. _V ) )
164 128 adantr 
 |-  ( ( ( ( A < { z } C_ No )
165 31 ad3antrrr 
 |-  ( ( ( ( A < B C_ No )
166 simpr 
 |-  ( ( ( ( A < A. t e. { z } A. w e. B t
167 164 165 166 3jca 
 |-  ( ( ( ( A < ( { z } C_ No /\ B C_ No /\ A. t e. { z } A. w e. B t
168 brsslt 
 |-  ( { z } < ( ( { z } e. _V /\ B e. _V ) /\ ( { z } C_ No /\ B C_ No /\ A. t e. { z } A. w e. B t
169 163 167 168 sylanbrc 
 |-  ( ( ( ( A < { z } <
170 161 169 mtand 
 |-  ( ( ( A < -. A. t e. { z } A. w e. B t
171 rexnal 
 |-  ( E. t e. { z } -. A. w e. B t  -. A. t e. { z } A. w e. B t
172 170 171 sylibr 
 |-  ( ( ( A < E. t e. { z } -. A. w e. B t
173 vex 
 |-  z e. _V
174 breq1 
 |-  ( t = z -> ( t  z
175 174 ralbidv 
 |-  ( t = z -> ( A. w e. B t  A. w e. B z
176 175 notbid 
 |-  ( t = z -> ( -. A. w e. B t  -. A. w e. B z
177 173 176 rexsn 
 |-  ( E. t e. { z } -. A. w e. B t  -. A. w e. B z
178 172 177 sylib 
 |-  ( ( ( A < -. A. w e. B z
179 31 ad2antrr 
 |-  ( ( ( A < B C_ No )
180 179 sselda 
 |-  ( ( ( ( A < w e. No )
181 110 adantr 
 |-  ( ( ( ( A < z e. No )
182 slenlt 
 |-  ( ( w e. No /\ z e. No ) -> ( w <_s z <-> -. z
183 180 181 182 syl2anc 
 |-  ( ( ( ( A < ( w <_s z <-> -. z
184 183 rexbidva 
 |-  ( ( ( A < ( E. w e. B w <_s z <-> E. w e. B -. z
185 rexnal 
 |-  ( E. w e. B -. z  -. A. w e. B z
186 184 185 bitrdi 
 |-  ( ( ( A < ( E. w e. B w <_s z <-> -. A. w e. B z
187 178 186 mpbird 
 |-  ( ( ( A < E. w e. B w <_s z )
188 187 ralrimiva 
 |-  ( ( A < A. z e. ( _Right ` X ) E. w e. B w <_s z )
189 103 188 jca 
 |-  ( ( A < ( A. x e. ( _Left ` X ) E. y e. A x <_s y /\ A. z e. ( _Right ` X ) E. w e. B w <_s z ) )