Theorem cofcutr 28117

Description: If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋) and 𝐵 is coinitial with ( R ‘𝑋). Theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.)

Assertion

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

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

Proof of Theorem cofcutr

Dummy variables 𝑎 𝑏 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bdayon 27945	. . . . . . . . . 10 ⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On
2	1	onssneli 6478	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥) → ¬ ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
3		leftssold 28064	. . . . . . . . . . . . 13 ⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
5	4	sselda 3937	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ ( O ‘( bday ‘𝑋)))
6		bdayon 27945	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑋) ∈ On
7		leftssno 28066	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑋) ⊆ No
8	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ No )
9	8	sselda 3937	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ No )
10		oldbday 28094	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
11	6, 9, 10	sylancr 598	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
12	5, 11	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘𝑋))
13		simplr 780	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
14	13	fveq2d 6885	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
15	12, 14	eleqtrd 2865	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
16	2, 15	nsyl3 139	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
17		cutbday 27977	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
18	17	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
19		bdayfn 27941	. . . . . . . . . . 11 ⊢ bday Fn No
20		ssrab2 4034	. . . . . . . . . . 11 ⊢ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
21		sneq 4599	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → {𝑡} = {𝑥})
22	21	breq2d 5121	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑥}))
23	21	breq1d 5119	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → ({𝑡} <<s 𝐵 ↔ {𝑥} <<s 𝐵))
24	22, 23	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
25	9	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ No )
26		vsnex 5406	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ V
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ∈ V)
28		sltsex2 27957	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
29	28	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ∈ V)
30	9	snssd 4752	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ⊆ No )
31		sltsss2 27959	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
32	31	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ⊆ No )
33	9	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 ∈ No )
34		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 = (𝐴 |s 𝐵))
35		simpl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵)
36	35	cutscld 27976	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝐴 |s 𝐵) ∈ No )
37	34, 36	eqeltrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 ∈ No )
38	37	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 ∈ No )
39	32	sselda 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
40		leftval 28042	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
42	41	eleq2d 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
43		rabid 3437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
44	42, 43	bitrdi 290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
45	44	simplbda 504	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 <s 𝑋)
46	45	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑋)
47		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵))
48		cutcuts 27974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
49	48	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
50	49	simp3d 1162	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {(𝐴 |s 𝐵)} <<s 𝐵)
51		ovex 7443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 |s 𝐵) ∈ V
52	51	snid 4628	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}
53		sltssepc 27964	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
54	52, 53	mp3an2 1478	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
55	50, 54	sylan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
56	47, 55	eqbrtrd 5133	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 <s 𝑏)
57	33, 38, 39, 46, 56	ltstrd 27927	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
58	57	3adant2 1149	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
59		velsn 4605	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {𝑥} ↔ 𝑎 = 𝑥)
60		breq1 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
61	59, 60	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {𝑥} → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
62	61	3ad2ant2 1152	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
63	58, 62	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏)
64	27, 29, 30, 32, 63	sltsd 27961	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} <<s 𝐵)
65	64	anim1ci 627	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))
66	24, 25, 65	elrabd 3652	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
67		fnfvima 7231	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
68	19, 20, 66, 67	mp3an12i 1494	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
69		intss1 4928	. . . . . . . . . 10 ⊢ (( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑥))
70	68, 69	syl 18	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑥))
71	18, 70	eqsstrd 3971	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
72	16, 71	mtand 827	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ 𝐴 <<s {𝑥})
73		sltsex1 27956	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
74	73	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ∈ V)
75	74, 26	jctir 529	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ∈ V ∧ {𝑥} ∈ V))
76		sltsss1 27958	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
77	76	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ⊆ No )
78	9	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝑥 ∈ No )
79	78	snssd 4752	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → {𝑥} ⊆ No )
80		simpr 489	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
81	77, 79, 80	3jca 1146	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡))
82		brslts 27955	. . . . . . . 8 ⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)))
83	75, 81, 82	sylanbrc 594	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 <<s {𝑥})
84	72, 83	mtand 827	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
85		rexnal 3117	. . . . . . 7 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
86		ralcom 3293	. . . . . . 7 ⊢ (∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
87	85, 86	xchbinx 337	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
88	84, 87	sylibr 237	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
89		vex 3459	. . . . . 6 ⊢ 𝑥 ∈ V
90		breq2 5113	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥))
91	90	ralbidv 3188	. . . . . . 7 ⊢ (𝑡 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
92	91	notbid 321	. . . . . 6 ⊢ (𝑡 = 𝑥 → (¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
93	89, 92	rexsn 4648	. . . . 5 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
94	88, 93	sylib 221	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
95	76	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐴 ⊆ No )
96	95	sselda 3937	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No )
97		lenlts 27916	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
98	9, 96, 97	syl2an2r 697	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
99	98	rexbidva 3187	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥))
100		rexnal 3117	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
101	99, 100	bitrdi 290	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
102	94, 101	mpbird 260	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
103	102	ralrimiva 3157	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
104	1	onssneli 6478	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧) → ¬ ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
105		rightssold 28065	. . . . . . . . . . . . 13 ⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
107	106	sselda 3937	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ ( O ‘( bday ‘𝑋)))
108		rightssno 28067	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝑋) ⊆ No
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ No )
110	109	sselda 3937	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ No )
111		oldbday 28094	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑧 ∈ No ) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
112	6, 110, 111	sylancr 598	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
113	107, 112	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘𝑋))
114		simplr 780	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
115	114	fveq2d 6885	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
116	113, 115	eleqtrd 2865	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
117	104, 116	nsyl3 139	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
118	17	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
119		sneq 4599	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧})
120	119	breq2d 5121	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑧}))
121	119	breq1d 5119	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → ({𝑡} <<s 𝐵 ↔ {𝑧} <<s 𝐵))
122	120, 121	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)))
123	110	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ No )
124	73	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ∈ V)
125		vsnex 5406	. . . . . . . . . . . . . . 15 ⊢ {𝑧} ∈ V
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ∈ V)
127	76	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ⊆ No )
128	110	snssd 4752	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ⊆ No )
129	127	sselda 3937	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No )
130	37	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 ∈ No )
131	110	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ No )
132	48	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
133	132	simp2d 1161	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {(𝐴 |s 𝐵)})
134		sltssepc 27964	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) → 𝑎 <s (𝐴 |s 𝐵))
135	52, 134	mp3an3 1479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
136	133, 135	sylan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
137		simpllr 787	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵))
138	136, 137	breqtrrd 5139	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑋)
139		rightval 28043	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧})
141	140	eleq2d 2849	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}))
142		rabid 3437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧))
143	141, 142	bitrdi 290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧)))
144	143	simplbda 504	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 <s 𝑧)
145	144	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 <s 𝑧)
146	129, 130, 131, 138, 145	ltstrd 27927	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑧)
147	146	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑧)
148		velsn 4605	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {𝑧} ↔ 𝑏 = 𝑧)
149		breq2 5113	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑧 → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
150	148, 149	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {𝑧} → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
151	150	3ad2ant3 1153	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
152	147, 151	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑏)
153	124, 126, 127, 128, 152	sltsd 27961	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {𝑧})
154	153	anim1i 626	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))
155	122, 123, 154	elrabd 3652	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
156		fnfvima 7231	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
157	19, 20, 155, 156	mp3an12i 1494	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
158		intss1 4928	. . . . . . . . . 10 ⊢ (( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑧))
159	157, 158	syl 18	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑧))
160	118, 159	eqsstrd 3971	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
161	117, 160	mtand 827	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ {𝑧} <<s 𝐵)
162	28	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ∈ V)
163	162, 125	jctil 528	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ∈ V ∧ 𝐵 ∈ V))
164	128	adantr 485	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} ⊆ No )
165	31	ad3antrrr 742	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ⊆ No )
166		simpr 489	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
167	164, 165, 166	3jca 1146	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤))
168		brslts 27955	. . . . . . . 8 ⊢ ({𝑧} <<s 𝐵 ↔ (({𝑧} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)))
169	163, 167, 168	sylanbrc 594	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} <<s 𝐵)
170	161, 169	mtand 827	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
171		rexnal 3117	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
172	170, 171	sylibr 237	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
173		vex 3459	. . . . . 6 ⊢ 𝑧 ∈ V
174		breq1 5112	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤))
175	174	ralbidv 3188	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
176	175	notbid 321	. . . . . 6 ⊢ (𝑡 = 𝑧 → (¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
177	173, 176	rexsn 4648	. . . . 5 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
178	172, 177	sylib 221	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
179	31	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐵 ⊆ No )
180	179	sselda 3937	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No )
181	110	adantr 485	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ No )
182		lenlts 27916	. . . . . . 7 ⊢ ((𝑤 ∈ No ∧ 𝑧 ∈ No ) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
183	180, 181, 182	syl2anc 595	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
184	183	rexbidva 3187	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤))
185		rexnal 3117	. . . . 5 ⊢ (∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
186	184, 185	bitrdi 290	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
187	178, 186	mpbird 260	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
188	187	ralrimiva 3157	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
189	103, 188	jca 520	1 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089  {crab 3416  Vcvv 3455   ⊆ wss 3905  {csn 4589  ∩ cint 4912   class class class wbr 5109   “ cima 5664  Oncon0 6360   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410   No csur 27804   <s clts 27805   bday cbday 27806   ≤s cles 27908   <<s cslts 27950   |s ccuts 27952   O cold 28016   L cleft 28018   R cright 28019

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-1o 8449  df-2o 8450  df-no 27807  df-lts 27808  df-bday 27809  df-les 27909  df-slts 27951  df-cuts 27953  df-made 28020  df-old 28021  df-left 28023  df-right 28024

This theorem is referenced by:  cofcutr1d  28118  cofcutr2d  28119