Metamath Proof Explorer

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	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to A \|_{s} B = C \|_{s} D$

Proof

Step	Hyp	Ref	Expression
1		simp11	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to A ≪_{s} B$
2		simp2	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z)$
3		simp12	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to C \in 𝒫 No$
4		simp3l	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to \forall t \in C \exists u \in A t \leq_{s} u$
5		cutcuts	$⊢ A ≪_{s} B \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
6	1 5	syl	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
7	6	simp2d	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to A ≪_{s} \{A \|_{s} B\}$
8		cofslts	$⊢ (C \in 𝒫 No \land \forall t \in C \exists u \in A t \leq_{s} u \land A ≪_{s} \{A \|_{s} B\}) \to C ≪_{s} \{A \|_{s} B\}$
9	3 4 7 8	syl3anc	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to C ≪_{s} \{A \|_{s} B\}$
10		simp13	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to D \in 𝒫 No$
11		simp3r	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to \forall r \in D \exists s \in B s \leq_{s} r$
12	6	simp3d	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to \{A \|_{s} B\} ≪_{s} B$
13		coinitslts	$⊢ (D \in 𝒫 No \land \forall r \in D \exists s \in B s \leq_{s} r \land \{A \|_{s} B\} ≪_{s} B) \to \{A \|_{s} B\} ≪_{s} D$
14	10 11 12 13	syl3anc	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to \{A \|_{s} B\} ≪_{s} D$
15		cofcut1	$⊢ (A ≪_{s} B \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D)) \to A \|_{s} B = C \|_{s} D$
16	1 2 9 14 15	syl112anc	$⊢ ((A ≪_{s} B \land C \in 𝒫 No \land D \in 𝒫 No) \land (\forall x \in A \exists y \in C x \leq_{s} y \land \forall z \in B \exists w \in D w \leq_{s} z) \land (\forall t \in C \exists u \in A t \leq_{s} u \land \forall r \in D \exists s \in B s \leq_{s} r)) \to A \|_{s} B = C \|_{s} D$