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		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	|- ( _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		leftssno	|- ( _Left ` X ) C_ No
24	23 22	sselid	|- ( ( ( ( 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. ( _Left ` X ) /\ x <_s x ) -> E. y e. ( _Left ` X ) x <_s y )
29	22 26 28	syl2anc	|- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. y e. ( _Left ` X ) x <_s y )
30	29	ralrimiva	|- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. x e. A E. y e. ( _Left ` 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	|- ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
45	44	a1i	|- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
46	45	eleq2d	|- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _Right ` 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. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X
49	35 43 48	mpbir2and	|- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _Right ` X ) )
50		rightssno	|- ( _Right ` X ) C_ No
51	50 49	sselid	|- ( ( ( ( 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. ( _Right ` X ) /\ z <_s z ) -> E. w e. ( _Right ` X ) w <_s z )
56	49 53 55	syl2anc	|- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. w e. ( _Right ` X ) w <_s z )
57	56	ralrimiva	|- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. z e. B E. w e. ( _Right ` X ) w <_s z )
58	30 57	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 ) )