Theorem cofcutrtime 27919

Description: If 𝑋 is the cut of 𝐴 and 𝐵 and all of 𝐴 and 𝐵 are older than 𝑋, then ( L ‘𝑋) is cofinal with 𝐴 and ( R ‘𝑋) is coinitial with 𝐵. 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.)

Assertion

Ref	Expression
cofcutrtime	⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧))

Distinct variable groups:   𝑥,𝐴   𝑧,𝐴   𝑥,𝐵   𝑧,𝐵   𝑧,𝑤,𝑋   𝑥,𝑋,𝑦   𝑧,𝑋

Allowed substitution hints:   𝐴(𝑦,𝑤)   𝐵(𝑦,𝑤)

Proof of Theorem cofcutrtime

Step	Hyp	Ref	Expression
1		ssun1 4118	. . . . . . . 8 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		sstr 3930	. . . . . . . 8 ⊢ ((𝐴 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋))) → 𝐴 ⊆ ( O ‘( bday ‘𝑋)))
3	1, 2	mpan 691	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) → 𝐴 ⊆ ( O ‘( bday ‘𝑋)))
4	3	3ad2ant1 1134	. . . . . 6 ⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 ⊆ ( O ‘( bday ‘𝑋)))
5	4	sselda 3921	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ( O ‘( bday ‘𝑋)))
6		simpl2 1194	. . . . . . . . 9 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝐴 <<s 𝐵)
7		cutcuts 27773	. . . . . . . . 9 ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
8	6, 7	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
9	8	simp2d 1144	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝐴 <<s {(𝐴 |s 𝐵)})
10		simpr 484	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
11		ovex 7400	. . . . . . . . 9 ⊢ (𝐴 |s 𝐵) ∈ V
12	11	snid 4606	. . . . . . . 8 ⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}
13	12	a1i 11	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)})
14	9, 10, 13	sltssepcd 27764	. . . . . 6 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s (𝐴 |s 𝐵))
15		simpl3 1195	. . . . . 6 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵))
16	14, 15	breqtrrd 5113	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s 𝑋)
17		leftval 27841	. . . . . . . 8 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
18	17	a1i 11	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
19	18	eleq2d 2822	. . . . . 6 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
20		rabid 3410	. . . . . 6 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
21	19, 20	bitrdi 287	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
22	5, 16, 21	mpbir2and 714	. . . 4 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ( L ‘𝑋))
23	22	leftnod 27872	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ No )
24		lesid 27731	. . . . 5 ⊢ (𝑥 ∈ No → 𝑥 ≤s 𝑥)
25	23, 24	syl 17	. . . 4 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤s 𝑥)
26		breq2 5089	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑥 ≤s 𝑦 ↔ 𝑥 ≤s 𝑥))
27	26	rspcev 3564	. . . 4 ⊢ ((𝑥 ∈ ( L ‘𝑋) ∧ 𝑥 ≤s 𝑥) → ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦)
28	22, 25, 27	syl2anc 585	. . 3 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦)
29	28	ralrimiva 3129	. 2 ⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦)
30		ssun2 4119	. . . . . . . 8 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
31		sstr 3930	. . . . . . . 8 ⊢ ((𝐵 ⊆ (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋))) → 𝐵 ⊆ ( O ‘( bday ‘𝑋)))
32	30, 31	mpan 691	. . . . . . 7 ⊢ ((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) → 𝐵 ⊆ ( O ‘( bday ‘𝑋)))
33	32	3ad2ant1 1134	. . . . . 6 ⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐵 ⊆ ( O ‘( bday ‘𝑋)))
34	33	sselda 3921	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ( O ‘( bday ‘𝑋)))
35		simpl3 1195	. . . . . 6 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵))
36		simpl2 1194	. . . . . . . . 9 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝐴 <<s 𝐵)
37	36, 7	syl 17	. . . . . . . 8 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
38	37	simp3d 1145	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → {(𝐴 |s 𝐵)} <<s 𝐵)
39	12	a1i 11	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)})
40		simpr 484	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵)
41	38, 39, 40	sltssepcd 27764	. . . . . 6 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑧)
42	35, 41	eqbrtrd 5107	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑋 <s 𝑧)
43		rightval 27842	. . . . . . . 8 ⊢ ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}
44	43	a1i 11	. . . . . . 7 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧})
45	44	eleq2d 2822	. . . . . 6 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}))
46		rabid 3410	. . . . . 6 ⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧))
47	45, 46	bitrdi 287	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ ( R ‘𝑋) ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧)))
48	34, 42, 47	mpbir2and 714	. . . 4 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ( R ‘𝑋))
49	48	rightnod 27874	. . . . 5 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ No )
50		lesid 27731	. . . . 5 ⊢ (𝑧 ∈ No → 𝑧 ≤s 𝑧)
51	49, 50	syl 17	. . . 4 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑧 ≤s 𝑧)
52		breq1 5088	. . . . 5 ⊢ (𝑤 = 𝑧 → (𝑤 ≤s 𝑧 ↔ 𝑧 ≤s 𝑧))
53	52	rspcev 3564	. . . 4 ⊢ ((𝑧 ∈ ( R ‘𝑋) ∧ 𝑧 ≤s 𝑧) → ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)
54	48, 51, 53	syl2anc 585	. . 3 ⊢ ((((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ 𝐵) → ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)
55	54	ralrimiva 3129	. 2 ⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧)
56	29, 55	jca 511	1 ⊢ (((𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋)) ∧ 𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  {crab 3389   ∪ cun 3887   ⊆ wss 3889  {csn 4567   class class class wbr 5085  ‘cfv 6498  (class class class)co 7367   No csur 27603   <s clts 27604   bday cbday 27605   ≤s cles 27708   <<s cslts 27749   |s ccuts 27751   O cold 27815   L cleft 27817   R cright 27818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-1o 8405  df-2o 8406  df-no 27606  df-lts 27607  df-bday 27608  df-les 27709  df-slts 27750  df-cuts 27752  df-made 27819  df-old 27820  df-left 27822  df-right 27823

This theorem is referenced by:  cofcutrtime1d  27920  cofcutrtime2d  27921