Metamath Proof Explorer


Theorem cofcutr2d

Description: If X is the cut of A and B , then B is coinitial with ( _RightX ) . Second half of theorem 2.9 of Gonshor p. 12. (Contributed by Scott Fenton, 25-Sep-2024)

Ref Expression
Hypotheses cofcutrd.1 âŠĒ ( 𝜑 → ðī <<s ðĩ )
cofcutrd.2 âŠĒ ( 𝜑 → 𝑋 = ( ðī |s ðĩ ) )
Assertion cofcutr2d ( 𝜑 → ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ ð‘Ī ∈ ðĩ ð‘Ī â‰Ī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 simprd âŠĒ ( 𝜑 → ∀ 𝑧 ∈ ( R ‘ 𝑋 ) ∃ ð‘Ī ∈ ðĩ ð‘Ī â‰Īs 𝑧 )