Metamath Proof Explorer

Theorem cofcut1

Description: If C is cofinal with A and D is coinitial with B and the cut of A and B lies between C and D , then the cut of C and D is equal to the cut of A and B . Theorem 2.6 of Gonshor p. 10. (Contributed by Scott Fenton, 25-Sep-2024)

Ref Expression
Assertion cofcut1 
|- ( ( A < ( A |s B ) = ( C |s D ) )

Proof

Step Hyp Ref Expression
1 simp3l 
 |-  ( ( A < C <
2 simp3r 
 |-  ( ( A < { ( A |s B ) } <
3 simp1 
 |-  ( ( A < A <
4 scutbday 
 |-  ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
5 3 4 syl 
 |-  ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( A <
6 ssltex1 
 |-  ( A < A e. _V )
7 3 6 syl 
 |-  ( ( A < A e. _V )
8 7 ad2antrr 
 |-  ( ( ( ( A < A e. _V )
9 ssltss1 
 |-  ( A < A C_ No )
10 3 9 syl 
 |-  ( ( A < A C_ No )
11 10 ad2antrr 
 |-  ( ( ( ( A < A C_ No )
12 8 11 elpwd 
 |-  ( ( ( ( A < A e. ~P No )
13 simpl2l 
 |-  ( ( ( A < A. x e. A E. y e. C x <_s y )
14 13 adantr 
 |-  ( ( ( ( A < A. x e. A E. y e. C x <_s y )
15 simpr 
 |-  ( ( ( ( A < C <
16 cofsslt 
 |-  ( ( A e. ~P No /\ A. x e. A E. y e. C x <_s y /\ C < A <
17 12 14 15 16 syl3anc 
 |-  ( ( ( ( A < A <
18 17 ex 
 |-  ( ( ( A < ( C < A <
19 ssltex2 
 |-  ( A < B e. _V )
20 3 19 syl 
 |-  ( ( A < B e. _V )
21 20 ad2antrr 
 |-  ( ( ( ( A < B e. _V )
22 ssltss2 
 |-  ( A < B C_ No )
23 3 22 syl 
 |-  ( ( A < B C_ No )
24 23 ad2antrr 
 |-  ( ( ( ( A < B C_ No )
25 21 24 elpwd 
 |-  ( ( ( ( A < B e. ~P No )
26 simpl2r 
 |-  ( ( ( A < A. z e. B E. w e. D w <_s z )
27 26 adantr 
 |-  ( ( ( ( A < A. z e. B E. w e. D w <_s z )
28 simpr 
 |-  ( ( ( ( A < { t } <
29 coinitsslt 
 |-  ( ( B e. ~P No /\ A. z e. B E. w e. D w <_s z /\ { t } < { t } <
30 25 27 28 29 syl3anc 
 |-  ( ( ( ( A < { t } <
31 30 ex 
 |-  ( ( ( A < ( { t } < { t } <
32 18 31 anim12d 
 |-  ( ( ( A < ( ( C < ( A <
33 32 ss2rabdv 
 |-  ( ( A < { t e. No | ( C <
34 imass2 
 |-  ( { t e. No | ( C < ( bday " { t e. No | ( C <
35 intss 
 |-  ( ( bday " { t e. No | ( C < |^| ( bday " { t e. No | ( A <
36 33 34 35 3syl 
 |-  ( ( A < |^| ( bday " { t e. No | ( A <
37 5 36 eqsstrd 
 |-  ( ( A < ( bday ` ( A |s B ) ) C_ |^| ( bday " { t e. No | ( C <
38 bdayfn 
 |-  bday Fn No
39 ssrab2 
 |-  { t e. No | ( C <
40 sneq 
 |-  ( t = ( A |s B ) -> { t } = { ( A |s B ) } )
41 40 breq2d 
 |-  ( t = ( A |s B ) -> ( C < C <
42 40 breq1d 
 |-  ( t = ( A |s B ) -> ( { t } < { ( A |s B ) } <
43 41 42 anbi12d 
 |-  ( t = ( A |s B ) -> ( ( C < ( C <
44 3 scutcld 
 |-  ( ( A < ( A |s B ) e. No )
45 simp3 
 |-  ( ( A < ( C <
46 43 44 45 elrabd 
 |-  ( ( A < ( A |s B ) e. { t e. No | ( C <
47 fnfvima 
 |-  ( ( bday Fn No /\ { t e. No | ( C < ( bday ` ( A |s B ) ) e. ( bday " { t e. No | ( C <
48 38 39 46 47 mp3an12i 
 |-  ( ( A < ( bday ` ( A |s B ) ) e. ( bday " { t e. No | ( C <
49 intss1 
 |-  ( ( bday ` ( A |s B ) ) e. ( bday " { t e. No | ( C < |^| ( bday " { t e. No | ( C <
50 48 49 syl 
 |-  ( ( A < |^| ( bday " { t e. No | ( C <
51 37 50 eqssd 
 |-  ( ( A < ( bday ` ( A |s B ) ) = |^| ( bday " { t e. No | ( C <
52 ovex 
 |-  ( A |s B ) e. _V
53 52 snnz 
 |-  { ( A |s B ) } =/= (/)
54 sslttr 
 |-  ( ( C < C <
55 53 54 mp3an3 
 |-  ( ( C < C <
56 55 3ad2ant3 
 |-  ( ( A < C <
57 eqscut 
 |-  ( ( C < ( ( C |s D ) = ( A |s B ) <-> ( C <
58 56 44 57 syl2anc 
 |-  ( ( A < ( ( C |s D ) = ( A |s B ) <-> ( C <
59 1 2 51 58 mpbir3and 
 |-  ( ( A < ( C |s D ) = ( A |s B ) )
60 59 eqcomd 
 |-  ( ( A < ( A |s B ) = ( C |s D ) )