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		scutcut	$⊢ 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	ssltsepcd	$⊢ ((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		leftssno	$⊢ L (X) \subseteq No$
24	23 22	sselid	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land x \in A) \to x \in No$
25		slerflex	$⊢ x \in No \to x \leq_{s} x$
26	24 25	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$
27		breq2	$⊢ y = x \to (x \leq_{s} y \leftrightarrow x \leq_{s} x)$
28	27	rspcev	$⊢ (x \in L (X) \land x \leq_{s} x) \to \exists y \in L (X) x \leq_{s} y$
29	22 26 28	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$
30	29	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$
31		ssun2	$⊢ B \subseteq A \cup B$
32		sstr	$⊢ (B \subseteq A \cup B \land A \cup B \subseteq Old (bday (X))) \to B \subseteq Old (bday (X))$
33	31 32	mpan	$⊢ A \cup B \subseteq Old (bday (X)) \to B \subseteq Old (bday (X))$
34	33	3ad2ant1	$⊢ (A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \to B \subseteq Old (bday (X))$
35	34	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))$
36		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$
37		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$
38	37 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)$
39	38	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$
40	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\}$
41		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$
42	39 40 41	ssltsepcd	$⊢ ((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$
43	36 42	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$
44		rightval	$⊢ R (X) = \{z \in Old (bday (X)) \| X <_{s} z\}$
45	44	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\}$
46	45	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\})$
47		rabid	$⊢ z \in \{z \in Old (bday (X)) \| X <_{s} z\} \leftrightarrow (z \in Old (bday (X)) \land X <_{s} z)$
48	46 47	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))$
49	35 43 48	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)$
50		rightssno	$⊢ R (X) \subseteq No$
51	50 49	sselid	$⊢ ((A \cup B \subseteq Old (bday (X)) \land A ≪_{s} B \land X = A \|_{s} B) \land z \in B) \to z \in No$
52		slerflex	$⊢ z \in No \to z \leq_{s} z$
53	51 52	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$
54		breq1	$⊢ w = z \to (w \leq_{s} z \leftrightarrow z \leq_{s} z)$
55	54	rspcev	$⊢ (z \in R (X) \land z \leq_{s} z) \to \exists w \in R (X) w \leq_{s} z$
56	49 53 55	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$
57	56	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$
58	30 57	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