Theorem cofcutr1d

Description: If X is the cut of A and B , then A is cofinal with ( _LeftX ) . First half of theorem 2.9 of Gonshor p. 12. (Contributed by Scott Fenton, 23-Jan-2025)

	Ref	Expression
Hypotheses	cofcutrd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	cofcutrd.2	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
Assertion	cofcutr1d	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		cofcutrd.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		cofcutrd.2	⊢ ( 𝜑 → 𝑋 = ( 𝐴 |s 𝐵 ) )
3		cofcutr	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑋 = ( 𝐴 |s 𝐵 ) ) → ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ 𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ) )
5	4	simpld	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( L ‘ 𝑋 ) ∃ 𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 )