Theorem 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	Could not format assertion : No typesetting found for |- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A. x e. A E. y e. ( _Left ` X ) x <_s y /\ A. z e. B E. w e. ( _Right ` X ) w <_s z ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssun1	$$⊢A\subseteq A\cup B$$
2		sstr	$$⊢\left(A\subseteq A\cup B\wedge A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\right)\to A\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
3	1 2	mpan	$$⊢A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\to A\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
4	3	3ad2ant1	$$⊢\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to A\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
5	4	sselda	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
6		simpl2	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to A{\ll }_{s}B$$
7		scutcut	$$⊢A{\ll }_{s}B\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
8	6 7	syl	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
9	8	simp2d	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to A{\ll }_s\left\{A{|}_{s}B\right\}$$
10		simpr	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to x\in A$$
11		ovex	$$⊢A{|}_{s}B\in \mathrm{V}$$
12	11	snid	$$⊢A{|}_{s}B\in \left\{A{|}_{s}B\right\}$$
13	12	a1i	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to A{|}_{s}B\in \left\{A{|}_{s}B\right\}$$
14	9 10 13	ssltsepcd	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to x{<}_s\left(A{|}_{s}B\right)$$
15		simpl3	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to X=A{|}_{s}B$$
16	14 15	breqtrrd	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to x{<}_{s}X$$
17		leftval	Could not format ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
18	17	a1i	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x ( _Left ` X ) = { x e. ( _Old ` ( bday ` X ) ) | x
19	18	eleq2d	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x ( x e. ( _Left ` X ) <-> x e. { x e. ( _Old ` ( bday ` X ) ) | x
20		rabid	$$⊢x\in \left\{x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|x{<}_{s}X\right\}\leftrightarrow \left(x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge x{<}_{s}X\right)$$
21	19 20	bitrdi	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x ( x e. ( _Left ` X ) <-> ( x e. ( _Old ` ( bday ` X ) ) /\ x
22	5 16 21	mpbir2and	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. ( _Left ` X ) ) : No typesetting found for |- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < x e. ( _Left ` X ) ) with typecode |-
23		leftssno	Could not format ( _Left ` X ) C_ No : No typesetting found for |- ( _Left ` X ) C_ No with typecode |-
24	23 22	sselid	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to x\in \mathrm{No}$$
25		slerflex	$$⊢x\in \mathrm{No}\to x{\le }_{s}x$$
26	24 25	syl	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge x\in A\right)\to x{\le }_{s}x$$
27		breq2	$$⊢y=x\to \left(x{\le }_{s}y\leftrightarrow x{\le }_{s}x\right)$$
28	27	rspcev	Could not format ( ( x e. ( _Left ` X ) /\ x <_s x ) -> E. y e. ( _Left ` X ) x <_s y ) : No typesetting found for |- ( ( x e. ( _Left ` X ) /\ x <_s x ) -> E. y e. ( _Left ` X ) x <_s y ) with typecode |-
29	22 26 28	syl2anc	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. y e. ( _Left ` X ) x <_s y ) : No typesetting found for |- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. y e. ( _Left ` X ) x <_s y ) with typecode |-
30	29	ralrimiva	Could not format ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. x e. A E. y e. ( _Left ` X ) x <_s y ) : No typesetting found for |- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. x e. A E. y e. ( _Left ` X ) x <_s y ) with typecode |-
31		ssun2	$$⊢B\subseteq A\cup B$$
32		sstr	$$⊢\left(B\subseteq A\cup B\wedge A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\right)\to B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
33	31 32	mpan	$$⊢A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\to B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
34	33	3ad2ant1	$$⊢\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\to B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
35	34	sselda	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)$$
36		simpl3	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to X=A{|}_{s}B$$
37		simpl2	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to A{\ll }_{s}B$$
38	37 7	syl	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
39	38	simp3d	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to \left\{A{|}_{s}B\right\}{\ll }_{s}B$$
40	12	a1i	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to A{|}_{s}B\in \left\{A{|}_{s}B\right\}$$
41		simpr	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to z\in B$$
42	39 40 41	ssltsepcd	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to \left(A{|}_{s}B\right){<}_{s}z$$
43	36 42	eqbrtrd	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to X{<}_{s}z$$
44		rightval	Could not format ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
45	44	a1i	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
46	45	eleq2d	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _Right ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X ( z e. ( _Right ` X ) <-> z e. { z e. ( _Old ` ( bday ` X ) ) | X
47		rabid	$$⊢z\in \left\{z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|X{<}_{s}z\right\}\leftrightarrow \left(z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge X{<}_{s}z\right)$$
48	46 47	bitrdi	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( z e. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X ( z e. ( _Right ` X ) <-> ( z e. ( _Old ` ( bday ` X ) ) /\ X
49	35 43 48	mpbir2and	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _Right ` X ) ) : No typesetting found for |- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < z e. ( _Right ` X ) ) with typecode |-
50		rightssno	Could not format ( _Right ` X ) C_ No : No typesetting found for |- ( _Right ` X ) C_ No with typecode |-
51	50 49	sselid	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to z\in \mathrm{No}$$
52		slerflex	$$⊢z\in \mathrm{No}\to z{\le }_{s}z$$
53	51 52	syl	$$⊢\left(\left(A\cup B\subseteq \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\wedge A{\ll }_{s}B\wedge X=A{|}_{s}B\right)\wedge z\in B\right)\to z{\le }_{s}z$$
54		breq1	$$⊢w=z\to \left(w{\le }_{s}z\leftrightarrow z{\le }_{s}z\right)$$
55	54	rspcev	Could not format ( ( z e. ( _Right ` X ) /\ z <_s z ) -> E. w e. ( _Right ` X ) w <_s z ) : No typesetting found for |- ( ( z e. ( _Right ` X ) /\ z <_s z ) -> E. w e. ( _Right ` X ) w <_s z ) with typecode |-
56	49 53 55	syl2anc	Could not format ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. w e. ( _Right ` X ) w <_s z ) : No typesetting found for |- ( ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < E. w e. ( _Right ` X ) w <_s z ) with typecode |-
57	56	ralrimiva	Could not format ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. z e. B E. w e. ( _Right ` X ) w <_s z ) : No typesetting found for |- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < A. z e. B E. w e. ( _Right ` X ) w <_s z ) with typecode |-
58	30 57	jca	Could not format ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A. x e. A E. y e. ( _Left ` X ) x <_s y /\ A. z e. B E. w e. ( _Right ` X ) w <_s z ) ) : No typesetting found for |- ( ( ( A u. B ) C_ ( _Old ` ( bday ` X ) ) /\ A < ( A. x e. A E. y e. ( _Left ` X ) x <_s y /\ A. z e. B E. w e. ( _Right ` X ) w <_s z ) ) with typecode |-