Metamath Proof Explorer


Theorem cofcut1d

Description: If C is cofinal with A and D is coinitial with B and the cut of A and B lies between C and D , then the cut of C and D is equal to the cut of A and B . Theorem 2.6 of Gonshor p. 10. (Contributed by Scott Fenton, 23-Jan-2025)

Ref Expression
Hypotheses cofcut1d.1 âŠĒ ( 𝜑 → ðī <<s ðĩ )
cofcut1d.2 âŠĒ ( 𝜑 → ∀ ð‘Ĩ ∈ ðī ∃ ð‘Ķ ∈ ðķ ð‘Ĩ â‰Īs ð‘Ķ )
cofcut1d.3 âŠĒ ( 𝜑 → ∀ 𝑧 ∈ ðĩ ∃ ð‘Ī ∈ 𝐷 ð‘Ī â‰Īs 𝑧 )
cofcut1d.4 âŠĒ ( 𝜑 → ðķ <<s { ( ðī |s ðĩ ) } )
cofcut1d.5 âŠĒ ( 𝜑 → { ( ðī |s ðĩ ) } <<s 𝐷 )
Assertion cofcut1d ( 𝜑 → ( ðī |s ðĩ ) = ( ðķ |s 𝐷 ) )

Proof

Step Hyp Ref Expression
1 cofcut1d.1 âŠĒ ( 𝜑 → ðī <<s ðĩ )
2 cofcut1d.2 âŠĒ ( 𝜑 → ∀ ð‘Ĩ ∈ ðī ∃ ð‘Ķ ∈ ðķ ð‘Ĩ â‰Īs ð‘Ķ )
3 cofcut1d.3 âŠĒ ( 𝜑 → ∀ 𝑧 ∈ ðĩ ∃ ð‘Ī ∈ 𝐷 ð‘Ī â‰Īs 𝑧 )
4 cofcut1d.4 âŠĒ ( 𝜑 → ðķ <<s { ( ðī |s ðĩ ) } )
5 cofcut1d.5 âŠĒ ( 𝜑 → { ( ðī |s ðĩ ) } <<s 𝐷 )
6 cofcut1 âŠĒ ( ( ðī <<s ðĩ ∧ ( ∀ ð‘Ĩ ∈ ðī ∃ ð‘Ķ ∈ ðķ ð‘Ĩ â‰Īs ð‘Ķ ∧ ∀ 𝑧 ∈ ðĩ ∃ ð‘Ī ∈ 𝐷 ð‘Ī â‰Īs 𝑧 ) ∧ ( ðķ <<s { ( ðī |s ðĩ ) } ∧ { ( ðī |s ðĩ ) } <<s 𝐷 ) ) → ( ðī |s ðĩ ) = ( ðķ |s 𝐷 ) )
7 1 2 3 4 5 6 syl122anc âŠĒ ( 𝜑 → ( ðī |s ðĩ ) = ( ðķ |s 𝐷 ) )