Theorem cofcut2d

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

	Ref	Expression
Hypotheses	cofcut2d.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
	cofcut2d.2	⊢ ( 𝜑 → 𝐶 ∈ 𝒫 No )
	cofcut2d.3	⊢ ( 𝜑 → 𝐷 ∈ 𝒫 No )
	cofcut2d.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 )
	cofcut2d.5	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 )
	cofcut2d.6	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 )
	cofcut2d.7	⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 )
Assertion	cofcut2d	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		cofcut2d.1	⊢ ( 𝜑 → 𝐴 <<s 𝐵 )
2		cofcut2d.2	⊢ ( 𝜑 → 𝐶 ∈ 𝒫 No )
3		cofcut2d.3	⊢ ( 𝜑 → 𝐷 ∈ 𝒫 No )
4		cofcut2d.4	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 )
5		cofcut2d.5	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 )
6		cofcut2d.6	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 )
7		cofcut2d.7	⊢ ( 𝜑 → ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 )
8		cofcut2	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )
9	1 2 3 4 5 6 7 8	syl322anc	⊢ ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )