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 ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 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 cutcuts ⊢ ( 𝐴 <<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 sltssepcd ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 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 22 leftnod ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
24 lesid ⊢ ( 𝑥 ∈ No → 𝑥 ≤s 𝑥 )
25 23 24 syl ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤s 𝑥 )
26 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑥 ≤s 𝑦 ↔ 𝑥 ≤s 𝑥 ) )
27 26 rspcev ⊢ ( ( 𝑥 ∈ ( L ‘ 𝑋 ) ∧ 𝑥 ≤s 𝑥 ) → ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 )
28 22 25 27 syl2anc ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 )
29 28 ralrimiva ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 )
30 ssun2 ⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
31 sstr ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ) → 𝐵 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
32 30 31 mpan ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) → 𝐵 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
33 32 3ad2ant1 ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → 𝐵 ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
34 33 sselda ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
35 simpl3 ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 = ( 𝐴 |s 𝐵 ) )
36 simpl2 ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 <<s 𝐵 )
37 36 7 syl ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
38 37 simp3d ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
39 12 a1i ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) ∈ { ( 𝐴 |s 𝐵 ) } )
40 simpr ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
41 38 39 40 sltssepcd ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) <s 𝑧 )
42 35 41 eqbrtrd ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 <s 𝑧 )
43 rightval ⊢ ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 }
44 43 a1i ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( R ‘ 𝑋 ) = { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } )
45 44 eleq2d ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( R ‘ 𝑋 ) ↔ 𝑧 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } ) )
46 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑧 } ↔ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑧 ) )
47 45 46 bitrdi ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑧 ∈ ( R ‘ 𝑋 ) ↔ ( 𝑧 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑧 ) ) )
48 34 42 47 mpbir2and ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( R ‘ 𝑋 ) )
49 48 rightnod ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ No )
50 lesid ⊢ ( 𝑧 ∈ No → 𝑧 ≤s 𝑧 )
51 49 50 syl ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ≤s 𝑧 )
52 breq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ≤s 𝑧 ↔ 𝑧 ≤s 𝑧 ) )
53 52 rspcev ⊢ ( ( 𝑧 ∈ ( R ‘ 𝑋 ) ∧ 𝑧 ≤s 𝑧 ) → ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )
54 48 51 53 syl2anc ⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )
55 54 ralrimiva ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )
56 29 55 jca ⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 ) )