cofcutrtime

Description: If X is the cut of A and B and all of A and B are older than X , then (LeftX ) is cofinal with A and ( RightX ) is coinitial with B . Note: we will call a cut where all of the elements of the cut are older than the cut itself a "timely" cut. Part of Theorem 4.02(12) of Alling p. 125. (Contributed by Scott Fenton, 27-Sep-2024)

		Ref	Expression
	Assertion	cofcutrtime	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to (\forall x \in A \exists y \in L (X) x \leq_{s} y \land \forall z \in B \exists w \in R (X) w \leq_{s} z)$

Proof

Step	Hyp	Ref	Expression
1		ssun1	$⊢ A \subseteq A \cup B$
2		sstr	$⊢ (A \subseteq A \cup B \land A \cup B \subseteq Old (bday (X))) \to A \subseteq Old (bday (X))$
3	1 2	mpan	$⊢ A \cup B \subseteq Old (bday (X)) \to A \subseteq Old (bday (X))$
4	3	3ad2ant1	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to A \subseteq Old (bday (X))$
5	4	sselda	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x \in Old (bday (X))$
6		simpl2	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to A ≪_{s} B$
7		cutcuts	$⊢ A ≪_{s} B \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
8	6 7	syl	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
9	8	simp2d	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to A ≪_{s} \{A \|_{s} B\}$
10		simpr	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x \in A$
11		ovex	$⊢ A \|_{s} B \in V$
12	11	snid	$⊢ A \|_{s} B \in \{A \|_{s} B\}$
13	12	a1i	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to A \|_{s} B \in \{A \|_{s} B\}$
14	9 10 13	sltssepcd	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x <_{s} (A \|_{s} B)$
15		simpl3	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to X = A \|_{s} B$
16	14 15	breqtrrd	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x <_{s} X$
17		leftval	$⊢ L (X) = \{x \in Old (bday (X)) \| x <_{s} X\}$
18	17	a1i	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to L (X) = \{x \in Old (bday (X)) \| x <_{s} X\}$
19	18	eleq2d	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to (x \in L (X) \leftrightarrow x \in \{x \in Old (bday (X)) \| x <_{s} X\})$
20		rabid	$⊢ x \in \{x \in Old (bday (X)) \| x <_{s} X\} \leftrightarrow (x \in Old (bday (X)) \land x <_{s} X)$
21	19 20	bitrdi	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to (x \in L (X) \leftrightarrow (x \in Old (bday (X)) \land x <_{s} X))$
22	5 16 21	mpbir2and	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x \in L (X)$
23	22	leftnod	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x \in No$
24		lesid	$⊢ x \in No \to x \leq_{s} x$
25	23 24	syl	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x \leq_{s} x$
26		breq2	$⊢ y = x \to (x \leq_{s} y \leftrightarrow x \leq_{s} x)$
27	26	rspcev	$⊢ (x \in L (X) \land x \leq_{s} x) \to \exists y \in L (X) x \leq_{s} y$
28	22 25 27	syl2anc	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to \exists y \in L (X) x \leq_{s} y$
29	28	ralrimiva	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to \forall x \in A \exists y \in L (X) x \leq_{s} y$
30		ssun2	$⊢ B \subseteq A \cup B$
31		sstr	$⊢ (B \subseteq A \cup B \land A \cup B \subseteq Old (bday (X))) \to B \subseteq Old (bday (X))$
32	30 31	mpan	$⊢ A \cup B \subseteq Old (bday (X)) \to B \subseteq Old (bday (X))$
33	32	3ad2ant1	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to B \subseteq Old (bday (X))$
34	33	sselda	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to z \in Old (bday (X))$
35		simpl3	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to X = A \|_{s} B$
36		simpl2	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to A ≪_{s} B$
37	36 7	syl	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to (A \|_{s} B \in No \land A ≪_{s} \{A \|_{s} B\} \land \{A \|_{s} B\} ≪_{s} B)$
38	37	simp3d	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to \{A \|_{s} B\} ≪_{s} B$
39	12	a1i	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to A \|_{s} B \in \{A \|_{s} B\}$
40		simpr	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to z \in B$
41	38 39 40	sltssepcd	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to (A \|_{s} B) <_{s} z$
42	35 41	eqbrtrd	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to X <_{s} z$
43		rightval	$⊢ R (X) = \{z \in Old (bday (X)) \| X <_{s} z\}$
44	43	a1i	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to R (X) = \{z \in Old (bday (X)) \| X <_{s} z\}$
45	44	eleq2d	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to (z \in R (X) \leftrightarrow z \in \{z \in Old (bday (X)) \| X <_{s} z\})$
46		rabid	$⊢ z \in \{z \in Old (bday (X)) \| X <_{s} z\} \leftrightarrow (z \in Old (bday (X)) \land X <_{s} z)$
47	45 46	bitrdi	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to (z \in R (X) \leftrightarrow (z \in Old (bday (X)) \land X <_{s} z))$
48	34 42 47	mpbir2and	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to z \in R (X)$
49	48	rightnod	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to z \in No$
50		lesid	$⊢ z \in No \to z \leq_{s} z$
51	49 50	syl	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to z \leq_{s} z$
52		breq1	$⊢ w = z \to (w \leq_{s} z \leftrightarrow z \leq_{s} z)$
53	52	rspcev	$⊢ (z \in R (X) \land z \leq_{s} z) \to \exists w \in R (X) w \leq_{s} z$
54	48 51 53	syl2anc	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to \exists w \in R (X) w \leq_{s} z$
55	54	ralrimiva	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to \forall z \in B \exists w \in R (X) w \leq_{s} z$
56	29 55	jca	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to (\forall x \in A \exists y \in L (X) x \leq_{s} y \land \forall z \in B \exists w \in R (X) w \leq_{s} z)$

Metamath Proof Explorer

Theorem cofcutrtime

Proof