Metamath Proof Explorer

Theorem cofcutrtime

Description: If X is the cut of A and B and all of A and B are older than X , then (LeftX ) is cofinal with A and ( RightX ) is coinitial with B . Note: we will call a cut where all of the elements of the cut are older than the cut itself a "timely" cut. Part of Theorem 4.02(12) of Alling p. 125. (Contributed by Scott Fenton, 27-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 ssun1 
 |-  A C_ ( A u. B )
2 sstr 
 |-  ( ( A C_ ( A u. B ) /\ ( A u. B ) C_ ( _Old ` ( bday ` X ) ) ) -> A C_ ( _Old ` ( bday ` X ) ) )
3 1 2 mpan 
 |-  ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) -> A C_ ( _Old ` ( bday ` X ) ) )
4 3 3ad2ant1 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A C_ ( _Old ` ( bday ` X ) ) )
5 4 sselda 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. ( _Old ` ( bday ` X ) ) )
6 simpl2 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A <
7 cutcuts 
 |-  ( A < ( ( A |s B ) e. No /\ A <
8 6 7 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( ( A |s B ) e. No /\ A <
9 8 simp2d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A <
10 simpr 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. A )
11 ovex 
 |-  ( A |s B ) e. _V
12 11 snid 
 |-  ( A |s B ) e. { ( A |s B ) }
13 12 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A |s B ) e. { ( A |s B ) } )
14 9 10 13 sltssepcd 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x
15 simpl3 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < X = ( A |s B ) )
16 14 15 breqtrrd 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x
17 leftval 
 |-  ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
18 17 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
19 18 eleq2d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
20 rabid 
 |-  ( x e. { x e. ( _Old ` ( bday ` X ) ) | x  ( x e. ( _Old ` ( bday ` X ) ) /\ x
21 19 20 bitrdi 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
22 5 16 21 mpbir2and 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. ( _Left ` X ) )
23 22 leftnod 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. No )
24 lesid 
 |-  ( x e. No -> x <_s x )
25 23 24 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x <_s x )
26 breq2 
 |-  ( y = x -> ( x <_s y <-> x <_s x ) )
27 26 rspcev 
 |-  ( ( x e. ( _Left ` X ) /\ x <_s x ) -> E. y e. ( _Left ` X ) x <_s y )
28 22 25 27 syl2anc 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. y e. ( _Left ` X ) x <_s y )
29 28 ralrimiva 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. x e. A E. y e. ( _Left ` X ) x <_s y )
30 ssun2 
 |-  B C_ ( A u. B )
31 sstr 
 |-  ( ( B C_ ( A u. B ) /\ ( A u. B ) C_ ( _Old ` ( bday ` X ) ) ) -> B C_ ( _Old ` ( bday ` X ) ) )
32 30 31 mpan 
 |-  ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) -> B C_ ( _Old ` ( bday ` X ) ) )
33 32 3ad2ant1 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < B C_ ( _Old ` ( bday ` X ) ) )
34 33 sselda 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _Old ` ( bday ` X ) ) )
35 simpl3 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < X = ( A |s B ) )
36 simpl2 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A <
37 36 7 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( ( A |s B ) e. No /\ A <
38 37 simp3d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < { ( A |s B ) } <
39 12 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A |s B ) e. { ( A |s B ) } )
40 simpr 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. B )
41 38 39 40 sltssepcd 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A |s B )
42 35 41 eqbrtrd 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < X
43 rightval 
 |-  ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
44 43 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
45 44 eleq2d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _Right ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X
46 rabid 
 |-  ( z e. { z e. ( _Old ` ( bday ` X ) ) | X  ( z e. ( _Old ` ( bday ` X ) ) /\ X
47 45 46 bitrdi 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X
48 34 42 47 mpbir2and 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _Right ` X ) )
49 48 rightnod 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. No )
50 lesid 
 |-  ( z e. No -> z <_s z )
51 49 50 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z <_s z )
52 breq1 
 |-  ( w = z -> ( w <_s z <-> z <_s z ) )
53 52 rspcev 
 |-  ( ( z e. ( _Right ` X ) /\ z <_s z ) -> E. w e. ( _Right ` X ) w <_s z )
54 48 51 53 syl2anc 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. w e. ( _Right ` X ) w <_s z )
55 54 ralrimiva 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. z e. B E. w e. ( _Right ` X ) w <_s z )
56 29 55 jca 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A. x e. A E. y e. ( _Left ` X ) x <_s y /\ A. z e. B E. w e. ( _Right ` X ) w <_s z ) )