cofcut1

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

		Ref	Expression
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		simp3l	$⊢ (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 C ≪_{s} \{A \|_{s} B\}$
2		simp3r	$⊢ (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\} ≪_{s} D$
3		simp1	$⊢ (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$
4		scutbday	$⊢ A ≪_{s} B \to bday (A \|_{s} B) = ⋂ bday [\{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}]$
5	3 4	syl	$⊢ (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 bday (A \|_{s} B) = ⋂ bday [\{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}]$
6		ssltex1	$⊢ A ≪_{s} B \to A \in V$
7	3 6	syl	$⊢ (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 \in V$
8	7	ad2antrr	$⊢ (((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)) \land t \in No) \land C ≪_{s} \{t\}) \to A \in V$
9		ssltss1	$⊢ A ≪_{s} B \to A \subseteq No$
10	3 9	syl	$⊢ (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 \subseteq No$
11	10	ad2antrr	$⊢ (((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)) \land t \in No) \land C ≪_{s} \{t\}) \to A \subseteq No$
12	8 11	elpwd	$⊢ (((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)) \land t \in No) \land C ≪_{s} \{t\}) \to A \in 𝒫 No$
13		simpl2l	$⊢ ((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)) \land t \in No) \to \forall x \in A \exists y \in C x \leq_{s} y$
14	13	adantr	$⊢ (((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)) \land t \in No) \land C ≪_{s} \{t\}) \to \forall x \in A \exists y \in C x \leq_{s} y$
15		simpr	$⊢ (((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)) \land t \in No) \land C ≪_{s} \{t\}) \to C ≪_{s} \{t\}$
16		cofsslt	$⊢ (A \in 𝒫 No \land \forall x \in A \exists y \in C x \leq_{s} y \land C ≪_{s} \{t\}) \to A ≪_{s} \{t\}$
17	12 14 15 16	syl3anc	$⊢ (((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)) \land t \in No) \land C ≪_{s} \{t\}) \to A ≪_{s} \{t\}$
18	17	ex	$⊢ ((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)) \land t \in No) \to (C ≪_{s} \{t\} \to A ≪_{s} \{t\})$
19		ssltex2	$⊢ A ≪_{s} B \to B \in V$
20	3 19	syl	$⊢ (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 B \in V$
21	20	ad2antrr	$⊢ (((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)) \land t \in No) \land \{t\} ≪_{s} D) \to B \in V$
22		ssltss2	$⊢ A ≪_{s} B \to B \subseteq No$
23	3 22	syl	$⊢ (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 B \subseteq No$
24	23	ad2antrr	$⊢ (((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)) \land t \in No) \land \{t\} ≪_{s} D) \to B \subseteq No$
25	21 24	elpwd	$⊢ (((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)) \land t \in No) \land \{t\} ≪_{s} D) \to B \in 𝒫 No$
26		simpl2r	$⊢ ((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)) \land t \in No) \to \forall z \in B \exists w \in D w \leq_{s} z$
27	26	adantr	$⊢ (((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)) \land t \in No) \land \{t\} ≪_{s} D) \to \forall z \in B \exists w \in D w \leq_{s} z$
28		simpr	$⊢ (((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)) \land t \in No) \land \{t\} ≪_{s} D) \to \{t\} ≪_{s} D$
29		coinitsslt	$⊢ (B \in 𝒫 No \land \forall z \in B \exists w \in D w \leq_{s} z \land \{t\} ≪_{s} D) \to \{t\} ≪_{s} B$
30	25 27 28 29	syl3anc	$⊢ (((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)) \land t \in No) \land \{t\} ≪_{s} D) \to \{t\} ≪_{s} B$
31	30	ex	$⊢ ((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)) \land t \in No) \to (\{t\} ≪_{s} D \to \{t\} ≪_{s} B)$
32	18 31	anim12d	$⊢ ((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)) \land t \in No) \to ((C ≪_{s} \{t\} \land \{t\} ≪_{s} D) \to (A ≪_{s} \{t\} \land \{t\} ≪_{s} B))$
33	32	ss2rabdv	$⊢ (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 \{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\} \subseteq \{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}$
34		imass2	$⊢ \{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\} \subseteq \{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\} \to bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}] \subseteq bday [\{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}]$
35		intss	$⊢ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}] \subseteq bday [\{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}] \to ⋂ bday [\{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}] \subseteq ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]$
36	33 34 35	3syl	$⊢ (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 ⋂ bday [\{t \in No \| (A ≪_{s} \{t\} \land \{t\} ≪_{s} B)\}] \subseteq ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]$
37	5 36	eqsstrd	$⊢ (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 bday (A \|_{s} B) \subseteq ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]$
38		bdayfn	$⊢ bday Fn No$
39		ssrab2	$⊢ \{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\} \subseteq No$
40		sneq	$⊢ t = A \|_{s} B \to \{t\} = \{A \|_{s} B\}$
41	40	breq2d	$⊢ t = A \|_{s} B \to (C ≪_{s} \{t\} \leftrightarrow C ≪_{s} \{A \|_{s} B\})$
42	40	breq1d	$⊢ t = A \|_{s} B \to (\{t\} ≪_{s} D \leftrightarrow \{A \|_{s} B\} ≪_{s} D)$
43	41 42	anbi12d	$⊢ t = A \|_{s} B \to ((C ≪_{s} \{t\} \land \{t\} ≪_{s} D) \leftrightarrow (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D))$
44	3	scutcld	$⊢ (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 \in No$
45		simp3	$⊢ (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 (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D)$
46	43 44 45	elrabd	$⊢ (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 \in \{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}$
47		fnfvima	$⊢ (bday Fn No \land \{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\} \subseteq No \land A \|_{s} B \in \{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}) \to bday (A \|_{s} B) \in bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]$
48	38 39 46 47	mp3an12i	$⊢ (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 bday (A \|_{s} B) \in bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]$
49		intss1	$⊢ bday (A \|_{s} B) \in bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}] \to ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}] \subseteq bday (A \|_{s} B)$
50	48 49	syl	$⊢ (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 ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}] \subseteq bday (A \|_{s} B)$
51	37 50	eqssd	$⊢ (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 bday (A \|_{s} B) = ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]$
52		ovex	$⊢ A \|_{s} B \in V$
53	52	snnz	$⊢ \{A \|_{s} B\} \neq \emptyset$
54		sslttr	$⊢ (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D \land \{A \|_{s} B\} \neq \emptyset) \to C ≪_{s} D$
55	53 54	mp3an3	$⊢ (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D) \to C ≪_{s} D$
56	55	3ad2ant3	$⊢ (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 C ≪_{s} D$
57		eqscut	$⊢ (C ≪_{s} D \land A \|_{s} B \in No) \to (C \|_{s} D = A \|_{s} B \leftrightarrow (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D \land bday (A \|_{s} B) = ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]))$
58	56 44 57	syl2anc	$⊢ (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 (C \|_{s} D = A \|_{s} B \leftrightarrow (C ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} D \land bday (A \|_{s} B) = ⋂ bday [\{t \in No \| (C ≪_{s} \{t\} \land \{t\} ≪_{s} D)\}]))$
59	1 2 51 58	mpbir3and	$⊢ (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 C \|_{s} D = A \|_{s} B$
60	59	eqcomd	$⊢ (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$

Metamath Proof Explorer

Theorem cofcut1

Proof