Theorem cofcut2

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, 25-Sep-2024)

	Ref	Expression
Assertion	cofcut2	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		simp11	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → 𝐴 <<s 𝐵 )
2		simp2	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) )
3		simp12	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → 𝐶 ∈ 𝒫 No )
4		simp3l	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 )
5		cutcuts	⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
6	1 5	syl	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
7	6	simp2d	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
8		cofslts	⊢ ( ( 𝐶 ∈ 𝒫 No ∧ ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ) → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } )
9	3 4 7 8	syl3anc	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } )
10		simp13	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → 𝐷 ∈ 𝒫 No )
11		simp3r	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 )
12	6	simp3d	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
13		coinitslts	⊢ ( ( 𝐷 ∈ 𝒫 No ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 )
14	10 11 12 13	syl3anc	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 )
15		cofcut1	⊢ ( ( 𝐴 <<s 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )
16	1 2 9 14 15	syl112anc	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 ∈ 𝒫 No ∧ 𝐷 ∈ 𝒫 No ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐶 𝑥 ≤s 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ∃ 𝑤 ∈ 𝐷 𝑤 ≤s 𝑧 ) ∧ ( ∀ 𝑡 ∈ 𝐶 ∃ 𝑢 ∈ 𝐴 𝑡 ≤s 𝑢 ∧ ∀ 𝑟 ∈ 𝐷 ∃ 𝑠 ∈ 𝐵 𝑠 ≤s 𝑟 ) ) → ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) )