Theorem cofcutrtime2d

Description: If X is a timely cut of A and B , then ( _RightX ) is coinitial with B . (Contributed by Scott Fenton, 23-Jan-2025)

	Ref	Expression
Hypotheses	cofcutrtimed.1	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
	cofcutrtimed.2	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	cofcutrtimed.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
Assertion	cofcutrtime2d	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		cofcutrtimed.1	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) )
2		cofcutrtimed.2	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
3		cofcutrtimed.3	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
4		cofcutrtime	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 ) )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( L ‘ 𝑋 ) 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 ) )
6	5	simprd	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ ( R ‘ 𝑋 ) 𝑤 ≤s 𝑧 )