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 (LX ) is cofinal with A and ( RX ) 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. ( _L ` X ) x <_s y /\ A. z e. B E. w e. ( _R ` 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 scutcut 
 |-  ( 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 ssltsepcd 
 |-  ( ( ( ( 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 
 |-  ( _L ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
18 17 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _L ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
19 18 eleq2d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( x e. ( _L ` 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. ( _L ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
22 5 16 21 mpbir2and 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. ( _L ` X ) )
23 leftssno 
 |-  ( _L ` X ) C_ No
24 23 22 sseldi 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. No )
25 slerflex 
 |-  ( x e. No -> x <_s x )
26 24 25 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x <_s x )
27 breq2 
 |-  ( y = x -> ( x <_s y <-> x <_s x ) )
28 27 rspcev 
 |-  ( ( x e. ( _L ` X ) /\ x <_s x ) -> E. y e. ( _L ` X ) x <_s y )
29 22 26 28 syl2anc 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. y e. ( _L ` X ) x <_s y )
30 29 ralrimiva 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. x e. A E. y e. ( _L ` X ) x <_s y )
31 ssun2 
 |-  B C_ ( A u. B )
32 sstr 
 |-  ( ( B C_ ( A u. B ) /\ ( A u. B ) C_ ( _Old ` ( bday ` X ) ) ) -> B C_ ( _Old ` ( bday ` X ) ) )
33 31 32 mpan 
 |-  ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) -> B C_ ( _Old ` ( bday ` X ) ) )
34 33 3ad2ant1 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < B C_ ( _Old ` ( bday ` X ) ) )
35 34 sselda 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _Old ` ( bday ` X ) ) )
36 simpl3 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < X = ( A |s B ) )
37 simpl2 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A <
38 37 7 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( ( A |s B ) e. No /\ A <
39 38 simp3d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < { ( A |s B ) } <
40 12 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A |s B ) e. { ( A |s B ) } )
41 simpr 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. B )
42 39 40 41 ssltsepcd 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A |s B )
43 36 42 eqbrtrd 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < X
44 rightval 
 |-  ( _R ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
45 44 a1i 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _R ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
46 45 eleq2d 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _R ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X
47 rabid 
 |-  ( z e. { z e. ( _Old ` ( bday ` X ) ) | X  ( z e. ( _Old ` ( bday ` X ) ) /\ X
48 46 47 bitrdi 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _R ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X
49 35 43 48 mpbir2and 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _R ` X ) )
50 rightssno 
 |-  ( _R ` X ) C_ No
51 50 49 sseldi 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. No )
52 slerflex 
 |-  ( z e. No -> z <_s z )
53 51 52 syl 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z <_s z )
54 breq1 
 |-  ( w = z -> ( w <_s z <-> z <_s z ) )
55 54 rspcev 
 |-  ( ( z e. ( _R ` X ) /\ z <_s z ) -> E. w e. ( _R ` X ) w <_s z )
56 49 53 55 syl2anc 
 |-  ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. w e. ( _R ` X ) w <_s z )
57 56 ralrimiva 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. z e. B E. w e. ( _R ` X ) w <_s z )
58 30 57 jca 
 |-  ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A. x e. A E. y e. ( _L ` X ) x <_s y /\ A. z e. B E. w e. ( _R ` X ) w <_s z ) )