Theorem cofcutr 28017

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 27845	. . . . . . . . . 10 ⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On
2	1	onssneli 6463	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥) → ¬ ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
3		leftssold 27964	. . . . . . . . . . . . 13 ⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
5	4	sselda 3936	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ ( O ‘( bday ‘𝑋)))
6		bdayon 27845	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑋) ∈ On
7		leftssno 27966	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑋) ⊆ No
8	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ No )
9	8	sselda 3936	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ No )
10		oldbday 27994	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
11	6, 9, 10	sylancr 596	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
12	5, 11	mpbid 234	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘𝑋))
13		simplr 778	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
14	13	fveq2d 6871	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
15	12, 14	eleqtrd 2864	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
16	2, 15	nsyl3 138	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
17		cutbday 27877	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
18	17	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
19		bdayfn 27841	. . . . . . . . . . 11 ⊢ bday Fn No
20		ssrab2 4033	. . . . . . . . . . 11 ⊢ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
21		sneq 4592	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → {𝑡} = {𝑥})
22	21	breq2d 5112	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑥}))
23	21	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → ({𝑡} <<s 𝐵 ↔ {𝑥} <<s 𝐵))
24	22, 23	anbi12d 641	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
25	9	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ No )
26		vsnex 5392	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ V
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ∈ V)
28		sltsex2 27857	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
29	28	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ∈ V)
30	9	snssd 4745	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ⊆ No )
31		sltsss2 27859	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
32	31	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ⊆ No )
33	9	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 ∈ No )
34		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 = (𝐴 |s 𝐵))
35		simpl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵)
36	35	cutscld 27876	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝐴 |s 𝐵) ∈ No )
37	34, 36	eqeltrd 2862	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 ∈ No )
38	37	ad2antrr 736	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 ∈ No )
39	32	sselda 3936	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
40		leftval 27942	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
42	41	eleq2d 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
43		rabid 3435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
44	42, 43	bitrdi 289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋)))
45	44	simplbda 503	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 <s 𝑋)
46	45	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑋)
47		simpllr 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵))
48		cutcuts 27874	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
49	48	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
50	49	simp3d 1157	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {(𝐴 |s 𝐵)} <<s 𝐵)
51		ovex 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 |s 𝐵) ∈ V
52	51	snid 4621	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}
53		sltssepc 27864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
54	52, 53	mp3an2 1470	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
55	50, 54	sylan 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
56	47, 55	eqbrtrd 5122	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 <s 𝑏)
57	33, 38, 39, 46, 56	ltstrd 27827	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
58	57	3adant2 1144	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
59		velsn 4598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {𝑥} ↔ 𝑎 = 𝑥)
60		breq1 5103	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
61	59, 60	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {𝑥} → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
62	61	3ad2ant2 1147	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
63	58, 62	mpbird 259	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏)
64	27, 29, 30, 32, 63	sltsd 27861	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} <<s 𝐵)
65	64	anim1ci 625	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))
66	24, 25, 65	elrabd 3652	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
67		fnfvima 7217	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
68	19, 20, 66, 67	mp3an12i 1486	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
69		intss1 4921	. . . . . . . . . 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 3970	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
72	16, 71	mtand 825	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ 𝐴 <<s {𝑥})
73		sltsex1 27856	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
74	73	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ∈ V)
75	74, 26	jctir 528	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ∈ V ∧ {𝑥} ∈ V))
76		sltsss1 27858	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
77	76	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ⊆ No )
78	9	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝑥 ∈ No )
79	78	snssd 4745	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → {𝑥} ⊆ No )
80		simpr 488	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
81	77, 79, 80	3jca 1141	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡))
82		brslts 27855	. . . . . . . 8 ⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)))
83	75, 81, 82	sylanbrc 592	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 <<s {𝑥})
84	72, 83	mtand 825	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
85		rexnal 3114	. . . . . . 7 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
86		ralcom 3290	. . . . . . 7 ⊢ (∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
87	85, 86	xchbinx 336	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
88	84, 87	sylibr 236	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
89		vex 3458	. . . . . 6 ⊢ 𝑥 ∈ V
90		breq2 5104	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥))
91	90	ralbidv 3185	. . . . . . 7 ⊢ (𝑡 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
92	91	notbid 320	. . . . . 6 ⊢ (𝑡 = 𝑥 → (¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
93	89, 92	rexsn 4641	. . . . 5 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
94	88, 93	sylib 220	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
95	76	ad2antrr 736	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐴 ⊆ No )
96	95	sselda 3936	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No )
97		lenlts 27816	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
98	9, 96, 97	syl2an2r 695	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
99	98	rexbidva 3184	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥))
100		rexnal 3114	. . . . 5 ⊢ (∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
101	99, 100	bitrdi 289	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
102	94, 101	mpbird 259	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
103	102	ralrimiva 3154	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
104	1	onssneli 6463	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧) → ¬ ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
105		rightssold 27965	. . . . . . . . . . . . 13 ⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
107	106	sselda 3936	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ ( O ‘( bday ‘𝑋)))
108		rightssno 27967	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝑋) ⊆ No
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ No )
110	109	sselda 3936	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ No )
111		oldbday 27994	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑧 ∈ No ) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
112	6, 110, 111	sylancr 596	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
113	107, 112	mpbid 234	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘𝑋))
114		simplr 778	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
115	114	fveq2d 6871	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
116	113, 115	eleqtrd 2864	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
117	104, 116	nsyl3 138	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
118	17	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
119		sneq 4592	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧})
120	119	breq2d 5112	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑧}))
121	119	breq1d 5110	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → ({𝑡} <<s 𝐵 ↔ {𝑧} <<s 𝐵))
122	120, 121	anbi12d 641	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)))
123	110	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ No )
124	73	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ∈ V)
125		vsnex 5392	. . . . . . . . . . . . . . 15 ⊢ {𝑧} ∈ V
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ∈ V)
127	76	ad2antrr 736	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ⊆ No )
128	110	snssd 4745	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ⊆ No )
129	127	sselda 3936	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No )
130	37	ad2antrr 736	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 ∈ No )
131	110	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ No )
132	48	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
133	132	simp2d 1156	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {(𝐴 |s 𝐵)})
134		sltssepc 27864	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) → 𝑎 <s (𝐴 |s 𝐵))
135	52, 134	mp3an3 1471	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
136	133, 135	sylan 589	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
137		simpllr 785	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵))
138	136, 137	breqtrrd 5128	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑋)
139		rightval 27943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧})
141	140	eleq2d 2848	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}))
142		rabid 3435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧))
143	141, 142	bitrdi 289	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧)))
144	143	simplbda 503	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 <s 𝑧)
145	144	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 <s 𝑧)
146	129, 130, 131, 138, 145	ltstrd 27827	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑧)
147	146	3adant3 1145	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑧)
148		velsn 4598	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {𝑧} ↔ 𝑏 = 𝑧)
149		breq2 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑧 → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
150	148, 149	sylbi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {𝑧} → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
151	150	3ad2ant3 1148	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
152	147, 151	mpbird 259	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑏)
153	124, 126, 127, 128, 152	sltsd 27861	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {𝑧})
154	153	anim1i 624	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))
155	122, 123, 154	elrabd 3652	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
156		fnfvima 7217	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
157	19, 20, 155, 156	mp3an12i 1486	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
158		intss1 4921	. . . . . . . . . 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 3970	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
161	117, 160	mtand 825	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ {𝑧} <<s 𝐵)
162	28	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ∈ V)
163	162, 125	jctil 527	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ∈ V ∧ 𝐵 ∈ V))
164	128	adantr 484	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} ⊆ No )
165	31	ad3antrrr 740	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ⊆ No )
166		simpr 488	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
167	164, 165, 166	3jca 1141	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤))
168		brslts 27855	. . . . . . . 8 ⊢ ({𝑧} <<s 𝐵 ↔ (({𝑧} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)))
169	163, 167, 168	sylanbrc 592	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} <<s 𝐵)
170	161, 169	mtand 825	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
171		rexnal 3114	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
172	170, 171	sylibr 236	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
173		vex 3458	. . . . . 6 ⊢ 𝑧 ∈ V
174		breq1 5103	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤))
175	174	ralbidv 3185	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
176	175	notbid 320	. . . . . 6 ⊢ (𝑡 = 𝑧 → (¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
177	173, 176	rexsn 4641	. . . . 5 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
178	172, 177	sylib 220	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
179	31	ad2antrr 736	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐵 ⊆ No )
180	179	sselda 3936	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No )
181	110	adantr 484	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ No )
182		lenlts 27816	. . . . . . 7 ⊢ ((𝑤 ∈ No ∧ 𝑧 ∈ No ) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
183	180, 181, 182	syl2anc 593	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
184	183	rexbidva 3184	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤))
185		rexnal 3114	. . . . 5 ⊢ (∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
186	184, 185	bitrdi 289	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
187	178, 186	mpbird 259	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
188	187	ralrimiva 3154	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
189	103, 188	jca 519	1 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1098   = wceq 1560   ∈ wcel 2142  ∀wral 3076  ∃wrex 3086  {crab 3414  Vcvv 3454   ⊆ wss 3904  {csn 4582  ∩ cint 4905   class class class wbr 5100   “ cima 5650  Oncon0 6346   Fn wfn 6516  ‘cfv 6521  (class class class)co 7396   No csur 27704   <s clts 27705   bday cbday 27706   ≤s cles 27808   <<s cslts 27850   |s ccuts 27852   O cold 27916   L cleft 27918   R cright 27919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-2nd 7971  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-1o 8437  df-2o 8438  df-no 27707  df-lts 27708  df-bday 27709  df-les 27809  df-slts 27851  df-cuts 27853  df-made 27920  df-old 27921  df-left 27923  df-right 27924

This theorem is referenced by:  cofcutr1d  28018  cofcutr2d  28019