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	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
2		sstr	⊢ ( ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ) → 𝐴 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
3	1 2	mpan	⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝐴 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
4	3	3ad2ant1	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → 𝐴 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
5	4	sselda	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
6		simpl2	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 <<s 𝐵 )
7		scutcut	⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
8	6 7	syl	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
9	8	simp2d	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
10		simpr	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
11		ovex	⊢ ( 𝐴 |s 𝐵 ) ∈ V
12	11	snid	⊢ ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) }
13	12	a1i	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) } )
14	9 10 13	ssltsepcd	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 <s ( 𝐴 |s 𝐵 ) )
15		simpl3	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
16	14 15	breqtrrd	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 <s 𝑋 )
17		leftval	⊢ ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 }
18	17	a1i	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( L ‘ 𝑋 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } )
19	18	eleq2d	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ) )
20		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑥 <s 𝑋 } ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) )
21	19 20	bitrdi	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( L ‘ 𝑋 ) ↔ ( 𝑥 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑥 <s 𝑋 ) ) )
22	5 16 21	mpbir2and	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( L ‘ 𝑋 ) )
23		leftssno	⊢ ( L ‘ 𝑋 ) ⊆ No
24	23 22	sselid	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
25		slerflex	⊢ ( 𝑥 ∈ No → 𝑥 ≤s 𝑥 )
26	24 25	syl	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤s 𝑥 )
27		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ≤s 𝑦 ↔ 𝑥 ≤s 𝑥 ) )
28	27	rspcev	⊢ ( ( 𝑥 ∈ ( L ‘ 𝑋 ) ∧ 𝑥 ≤s 𝑥 ) → ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 )
29	22 26 28	syl2anc	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 )
30	29	ralrimiva	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 )
31		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
32		sstr	⊢ ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ) → 𝐵 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
33	31 32	mpan	⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝐵 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
34	33	3ad2ant1	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → 𝐵 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
35	34	sselda	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
36		simpl3	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
37		simpl2	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 <<s 𝐵 )
38	37 7	syl	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
39	38	simp3d	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
40	12	a1i	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) } )
41		simpr	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
42	39 40 41	ssltsepcd	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) <s 𝑧 )
43	36 42	eqbrtrd	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 <s 𝑧 )
44		rightval	⊢ ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 }
45	44	a1i	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } )
46	45	eleq2d	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( R ‘ 𝑋 ) ↔ 𝑧 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } ) )
47		rabid	⊢ ( 𝑧 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } ↔ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑧 ) )
48	46 47	bitrdi	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( R ‘ 𝑋 ) ↔ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑧 ) ) )
49	35 43 48	mpbir2and	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( R ‘ 𝑋 ) )
50		rightssno	⊢ ( R ‘ 𝑋 ) ⊆ No
51	50 49	sselid	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ No )
52		slerflex	⊢ ( 𝑧 ∈ No → 𝑧 ≤s 𝑧 )
53	51 52	syl	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ≤s 𝑧 )
54		breq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≤s 𝑧 ↔ 𝑧 ≤s 𝑧 ) )
55	54	rspcev	⊢ ( ( 𝑧 ∈ ( R ‘ 𝑋 ) ∧ 𝑧 ≤s 𝑧 ) → ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )
56	49 53 55	syl2anc	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )
57	56	ralrimiva	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )
58	30 57	jca	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 ) )