Theorem cofcutr 27934

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 27762	. . . . . . . . . 10 ⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On
2	1	onssneli 6427	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥) → ¬ ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
3		leftssold 27881	. . . . . . . . . . . . 13 ⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
5	4	sselda 3915	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ ( O ‘( bday ‘𝑋)))
6		bdayon 27762	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑋) ∈ On
7		leftssno 27883	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑋) ⊆ No
8	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ No )
9	8	sselda 3915	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ No )
10		oldbday 27911	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
11	6, 9, 10	sylancr 593	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
12	5, 11	mpbid 233	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘𝑋))
13		simplr 774	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
14	13	fveq2d 6831	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
15	12, 14	eleqtrd 2841	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
16	2, 15	nsyl3 138	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
17		cutbday 27794	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
18	17	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
19		bdayfn 27759	. . . . . . . . . . 11 ⊢ bday Fn No
20		ssrab2 4011	. . . . . . . . . . 11 ⊢ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
21		sneq 4565	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → {𝑡} = {𝑥})
22	21	breq2d 5084	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑥}))
23	21	breq1d 5082	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → ({𝑡} <<s 𝐵 ↔ {𝑥} <<s 𝐵))
24	22, 23	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
25	9	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ No )
26		vsnex 5364	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ V
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ∈ V)
28		sltsex2 27774	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
29	28	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ∈ V)
30	9	snssd 4718	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ⊆ No )
31		sltsss2 27776	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
32	31	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ⊆ No )
33	9	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 ∈ No )
34		simpr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 = (𝐴 |s 𝐵))
35		simpl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵)
36	35	cutscld 27793	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝐴 |s 𝐵) ∈ No )
37	34, 36	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 ∈ No )
38	37	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 ∈ No )
39	32	sselda 3915	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
40		leftval 27859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
42	41	eleq2d 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
43		rabid 3412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
44	42, 43	bitrdi 288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
45	44	simplbda 500	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 <s 𝑋)
46	45	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑋)
47		simpllr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵))
48		cutcuts 27791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
49	48	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
50	49	simp3d 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {(𝐴 |s 𝐵)} <<s 𝐵)
51		ovex 7389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 |s 𝐵) ∈ V
52	51	snid 4594	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}
53		sltssepc 27781	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
54	52, 53	mp3an2 1457	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
55	50, 54	sylan 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
56	47, 55	eqbrtrd 5094	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 <s 𝑏)
57	33, 38, 39, 46, 56	ltstrd 27745	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
58	57	3adant2 1137	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
59		velsn 4571	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {𝑥} ↔ 𝑎 = 𝑥)
60		breq1 5075	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
61	59, 60	sylbi 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {𝑥} → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
62	61	3ad2ant2 1140	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
63	58, 62	mpbird 258	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏)
64	27, 29, 30, 32, 63	sltsd 27778	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} <<s 𝐵)
65	64	anim1ci 622	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))
66	24, 25, 65	elrabd 3631	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
67		fnfvima 7177	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
68	19, 20, 66, 67	mp3an12i 1473	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
69		intss1 4893	. . . . . . . . . 10 ⊢ (( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑥))
70	68, 69	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑥))
71	18, 70	eqsstrd 3949	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
72	16, 71	mtand 821	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ 𝐴 <<s {𝑥})
73		sltsex1 27773	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
74	73	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ∈ V)
75	74, 26	jctir 525	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ∈ V ∧ {𝑥} ∈ V))
76		sltsss1 27775	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
77	76	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ⊆ No )
78	9	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝑥 ∈ No )
79	78	snssd 4718	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → {𝑥} ⊆ No )
80		simpr 485	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
81	77, 79, 80	3jca 1134	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡))
82		brslts 27772	. . . . . . . 8 ⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)))
83	75, 81, 82	sylanbrc 589	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 <<s {𝑥})
84	72, 83	mtand 821	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
85		rexnal 3091	. . . . . . 7 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
86		ralcom 3267	. . . . . . 7 ⊢ (∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
87	85, 86	xchbinx 335	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
88	84, 87	sylibr 235	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
89		vex 3435	. . . . . 6 ⊢ 𝑥 ∈ V
90		breq2 5076	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥))
91	90	ralbidv 3162	. . . . . . 7 ⊢ (𝑡 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
92	91	notbid 319	. . . . . 6 ⊢ (𝑡 = 𝑥 → (¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
93	89, 92	rexsn 4614	. . . . 5 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
94	88, 93	sylib 219	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
95	76	ad2antrr 732	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐴 ⊆ No )
96	95	sselda 3915	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No )
97		lenlts 27734	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
98	9, 96, 97	syl2an2r 691	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
99	98	rexbidva 3161	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥))
100		rexnal 3091	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
101	99, 100	bitrdi 288	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
102	94, 101	mpbird 258	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
103	102	ralrimiva 3131	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
104	1	onssneli 6427	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧) → ¬ ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
105		rightssold 27882	. . . . . . . . . . . . 13 ⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
107	106	sselda 3915	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ ( O ‘( bday ‘𝑋)))
108		rightssno 27884	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝑋) ⊆ No
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ No )
110	109	sselda 3915	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ No )
111		oldbday 27911	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑧 ∈ No ) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
112	6, 110, 111	sylancr 593	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
113	107, 112	mpbid 233	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘𝑋))
114		simplr 774	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
115	114	fveq2d 6831	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
116	113, 115	eleqtrd 2841	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
117	104, 116	nsyl3 138	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
118	17	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
119		sneq 4565	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧})
120	119	breq2d 5084	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑧}))
121	119	breq1d 5082	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → ({𝑡} <<s 𝐵 ↔ {𝑧} <<s 𝐵))
122	120, 121	anbi12d 638	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)))
123	110	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ No )
124	73	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ∈ V)
125		vsnex 5364	. . . . . . . . . . . . . . 15 ⊢ {𝑧} ∈ V
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ∈ V)
127	76	ad2antrr 732	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ⊆ No )
128	110	snssd 4718	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ⊆ No )
129	127	sselda 3915	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No )
130	37	ad2antrr 732	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 ∈ No )
131	110	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ No )
132	48	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
133	132	simp2d 1149	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {(𝐴 |s 𝐵)})
134		sltssepc 27781	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) → 𝑎 <s (𝐴 |s 𝐵))
135	52, 134	mp3an3 1458	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
136	133, 135	sylan 586	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
137		simpllr 781	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵))
138	136, 137	breqtrrd 5100	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑋)
139		rightval 27860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧})
141	140	eleq2d 2825	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}))
142		rabid 3412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧))
143	141, 142	bitrdi 288	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧)))
144	143	simplbda 500	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 <s 𝑧)
145	144	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 <s 𝑧)
146	129, 130, 131, 138, 145	ltstrd 27745	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑧)
147	146	3adant3 1138	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑧)
148		velsn 4571	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {𝑧} ↔ 𝑏 = 𝑧)
149		breq2 5076	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑧 → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
150	148, 149	sylbi 218	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {𝑧} → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
151	150	3ad2ant3 1141	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
152	147, 151	mpbird 258	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑏)
153	124, 126, 127, 128, 152	sltsd 27778	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {𝑧})
154	153	anim1i 621	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))
155	122, 123, 154	elrabd 3631	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
156		fnfvima 7177	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
157	19, 20, 155, 156	mp3an12i 1473	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
158		intss1 4893	. . . . . . . . . 10 ⊢ (( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑧))
159	157, 158	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) ⊆ ( bday ‘𝑧))
160	118, 159	eqsstrd 3949	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
161	117, 160	mtand 821	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ {𝑧} <<s 𝐵)
162	28	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ∈ V)
163	162, 125	jctil 524	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ∈ V ∧ 𝐵 ∈ V))
164	128	adantr 481	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} ⊆ No )
165	31	ad3antrrr 736	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ⊆ No )
166		simpr 485	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
167	164, 165, 166	3jca 1134	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤))
168		brslts 27772	. . . . . . . 8 ⊢ ({𝑧} <<s 𝐵 ↔ (({𝑧} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)))
169	163, 167, 168	sylanbrc 589	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} <<s 𝐵)
170	161, 169	mtand 821	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
171		rexnal 3091	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
172	170, 171	sylibr 235	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
173		vex 3435	. . . . . 6 ⊢ 𝑧 ∈ V
174		breq1 5075	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤))
175	174	ralbidv 3162	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
176	175	notbid 319	. . . . . 6 ⊢ (𝑡 = 𝑧 → (¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
177	173, 176	rexsn 4614	. . . . 5 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
178	172, 177	sylib 219	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
179	31	ad2antrr 732	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐵 ⊆ No )
180	179	sselda 3915	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No )
181	110	adantr 481	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ No )
182		lenlts 27734	. . . . . . 7 ⊢ ((𝑤 ∈ No ∧ 𝑧 ∈ No ) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
183	180, 181, 182	syl2anc 590	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
184	183	rexbidva 3161	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤))
185		rexnal 3091	. . . . 5 ⊢ (∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
186	184, 185	bitrdi 288	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
187	178, 186	mpbird 258	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
188	187	ralrimiva 3131	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
189	103, 188	jca 516	1 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  {crab 3391  Vcvv 3431   ⊆ wss 3883  {csn 4555  ∩ cint 4877   class class class wbr 5072   “ cima 5621  Oncon0 6310   Fn wfn 6480  ‘cfv 6485  (class class class)co 7356   No csur 27621   <s clts 27622   bday cbday 27623   ≤s cles 27726   <<s cslts 27767   |s ccuts 27769   O cold 27833   L cleft 27835   R cright 27836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-1o 8395  df-2o 8396  df-no 27624  df-lts 27625  df-bday 27626  df-les 27727  df-slts 27768  df-cuts 27770  df-made 27837  df-old 27838  df-left 27840  df-right 27841

This theorem is referenced by:  cofcutr1d  27935  cofcutr2d  27936