Theorem cofcutr 28319

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 28147	. . . . . . . . . 10 ⊢ (bday‘(𝐴 |s 𝐵)) ∈ On
2	1	onssneli 6483	. . . . . . . . 9 ⊢ ((bday‘(𝐴 |s 𝐵)) ⊆ (bday‘𝑥) → ¬ (bday‘𝑥) ∈ (bday‘(𝐴 |s 𝐵)))
3		leftssold 28266	. . . . . . . . . . . . 13 ⊢ (L‘𝑋) ⊆ (O‘(bday‘𝑋))
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (L‘𝑋) ⊆ (O‘(bday‘𝑋)))
5	4	sselda 3909	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝑥 ∈ (O‘(bday‘𝑋)))
6		bdayon 28147	. . . . . . . . . . . 12 ⊢ (bday‘𝑋) ∈ On
7		leftssno 28268	. . . . . . . . . . . . . 14 ⊢ (L‘𝑋) ⊆ No
8	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (L‘𝑋) ⊆ No)
9	8	sselda 3909	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝑥 ∈ No)
10		oldbday 28296	. . . . . . . . . . . 12 ⊢ (((bday‘𝑋) ∈ On ∧ 𝑥 ∈ No) → (𝑥 ∈ (O‘(bday‘𝑋)) ↔ (bday‘𝑥) ∈ (bday‘𝑋)))
11	6, 9, 10	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → (𝑥 ∈ (O‘(bday‘𝑋)) ↔ (bday‘𝑥) ∈ (bday‘𝑋)))
12	5, 11	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → (bday‘𝑥) ∈ (bday‘𝑋))
13		simplr 781	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
14	13	fveq2d 6894	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → (bday‘𝑋) = (bday‘(𝐴 |s 𝐵)))
15	12, 14	eleqtrd 2862	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → (bday‘𝑥) ∈ (bday‘(𝐴 |s 𝐵)))
16	2, 15	nsyl3 139	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ¬ (bday‘(𝐴 |s 𝐵)) ⊆ (bday‘𝑥))
17		cutbday 28179	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → (bday‘(𝐴 |s 𝐵)) = ∩ (bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
18	17	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (bday‘(𝐴 |s 𝐵)) = ∩ (bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
19		bdayfn 28143	. . . . . . . . . . 11 ⊢ bday Fn No
20		ssrab2 4004	. . . . . . . . . . 11 ⊢ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
21		sneq 4590	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → {𝑡} = {𝑥})
22	21	breq2d 5114	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑥}))
23	21	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → ({𝑡} <<s 𝐵 ↔ {𝑥} <<s 𝐵))
24	22, 23	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
25	9	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ No)
26		vsnex 5393	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ V
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → {𝑥} ∈ V)
28		sltsex2 28159	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
29	28	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝐵 ∈ V)
30	9	snssd 4743	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → {𝑥} ⊆ No)
31		sltsss2 28161	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No)
32	31	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝐵 ⊆ No)
33	9	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 ∈ No)
34		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 = (𝐴 |s 𝐵))
35		simpl 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝐴 <<s 𝐵)
36	35	cutscld 28178	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝐴 |s 𝐵) ∈ No)
37	34, 36	eqeltrd 2860	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 ∈ No)
38	37	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 ∈ No)
39	32	sselda 3909	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No)
40		leftval 28244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (L‘𝑋) = {𝑥 ∈ (O‘(bday‘𝑋)) ∣ 𝑥 <s 𝑋}
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (L‘𝑋) = {𝑥 ∈ (O‘(bday‘𝑋)) ∣ 𝑥 <s 𝑋})
42	41	eleq2d 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ (L‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ (O‘(bday‘𝑋)) ∣ 𝑥 <s 𝑋}))
43		rabid 3432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑥 ∈ (O‘(bday‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ (O‘(bday‘𝑋)) ∧ 𝑥 <s 𝑋))
44	42, 43	bitrdi 290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ (L‘𝑋) ↔ (𝑥 ∈ (O‘(bday‘𝑋)) ∧ 𝑥 <s 𝑋)))
45	44	simplbda 505	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝑥 <s 𝑋)
46	45	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑋)
47		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵))
48		cutcuts 28176	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
49	48	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
50	49	simp3d 1162	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → {(𝐴 |s 𝐵)} <<s 𝐵)
51		ovex 7457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 |s 𝐵) ∈ V
52	51	snid 4619	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}
53		sltssepc 28166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
54	52, 53	mp3an2 1478	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
55	50, 54	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
56	47, 55	eqbrtrd 5126	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 <s 𝑏)
57	33, 38, 39, 46, 56	ltstrd 28129	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
58	57	3adant2 1149	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
59		velsn 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {𝑥} ↔ 𝑎 = 𝑥)
60		breq1 5105	. . . . . . . . . . . . . . . . 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 28163	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → {𝑥} <<s 𝐵)
65	64	anim1ci 628	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))
66	24, 25, 65	elrabd 3646	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
67		fnfvima 7243	. . . . . . . . . . 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 4922	. . . . . . . . . 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 3943	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (bday‘(𝐴 |s 𝐵)) ⊆ (bday‘𝑥))
72	16, 71	mtand 828	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ¬ 𝐴 <<s {𝑥})
73		sltsex1 28158	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
74	73	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ∈ V)
75	74, 26	jctir 530	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ∈ V ∧ {𝑥} ∈ V))
76		sltsss1 28160	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No)
77	76	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ⊆ No)
78	9	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝑥 ∈ No)
79	78	snssd 4743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → {𝑥} ⊆ No)
80		simpr 490	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
81	77, 79, 80	3jca 1146	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡))
82		brslts 28157	. . . . . . . 8 ⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)))
83	75, 81, 82	sylanbrc 595	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 <<s {𝑥})
84	72, 83	mtand 828	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
85		rexnal 3114	. . . . . . 7 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
86		ralcom 3290	. . . . . . 7 ⊢ (∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
87	85, 86	xchbinx 337	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
88	84, 87	sylibr 237	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
89		vex 3454	. . . . . 6 ⊢ 𝑥 ∈ V
90		breq2 5106	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥))
91	90	ralbidv 3185	. . . . . . 7 ⊢ (𝑡 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
92	91	notbid 321	. . . . . 6 ⊢ (𝑡 = 𝑥 → (¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
93	89, 92	rexsn 4639	. . . . 5 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
94	88, 93	sylib 221	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
95	76	ad2antrr 739	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → 𝐴 ⊆ No)
96	95	sselda 3909	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No)
97		lenlts 28118	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
98	9, 96, 97	syl2an2r 698	. . . . . 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 290	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
102	94, 101	mpbird 260	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ (L‘𝑋)) → ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
103	102	ralrimiva 3154	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ (L‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
104	1	onssneli 6483	. . . . . . . . 9 ⊢ ((bday‘(𝐴 |s 𝐵)) ⊆ (bday‘𝑧) → ¬ (bday‘𝑧) ∈ (bday‘(𝐴 |s 𝐵)))
105		rightssold 28267	. . . . . . . . . . . . 13 ⊢ (R‘𝑋) ⊆ (O‘(bday‘𝑋))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (R‘𝑋) ⊆ (O‘(bday‘𝑋)))
107	106	sselda 3909	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝑧 ∈ (O‘(bday‘𝑋)))
108		rightssno 28269	. . . . . . . . . . . . . 14 ⊢ (R‘𝑋) ⊆ No
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (R‘𝑋) ⊆ No)
110	109	sselda 3909	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝑧 ∈ No)
111		oldbday 28296	. . . . . . . . . . . 12 ⊢ (((bday‘𝑋) ∈ On ∧ 𝑧 ∈ No) → (𝑧 ∈ (O‘(bday‘𝑋)) ↔ (bday‘𝑧) ∈ (bday‘𝑋)))
112	6, 110, 111	sylancr 599	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → (𝑧 ∈ (O‘(bday‘𝑋)) ↔ (bday‘𝑧) ∈ (bday‘𝑋)))
113	107, 112	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → (bday‘𝑧) ∈ (bday‘𝑋))
114		simplr 781	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
115	114	fveq2d 6894	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → (bday‘𝑋) = (bday‘(𝐴 |s 𝐵)))
116	113, 115	eleqtrd 2862	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → (bday‘𝑧) ∈ (bday‘(𝐴 |s 𝐵)))
117	104, 116	nsyl3 139	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ¬ (bday‘(𝐴 |s 𝐵)) ⊆ (bday‘𝑧))
118	17	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ {𝑧} <<s 𝐵) → (bday‘(𝐴 |s 𝐵)) = ∩ (bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
119		sneq 4590	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧})
120	119	breq2d 5114	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑧}))
121	119	breq1d 5112	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → ({𝑡} <<s 𝐵 ↔ {𝑧} <<s 𝐵))
122	120, 121	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)))
123	110	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ No)
124	73	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝐴 ∈ V)
125		vsnex 5393	. . . . . . . . . . . . . . 15 ⊢ {𝑧} ∈ V
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → {𝑧} ∈ V)
127	76	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝐴 ⊆ No)
128	110	snssd 4743	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → {𝑧} ⊆ No)
129	127	sselda 3909	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No)
130	37	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 ∈ No)
131	110	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ No)
132	48	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
133	132	simp2d 1161	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝐴 <<s {(𝐴 |s 𝐵)})
134		sltssepc 28166	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) → 𝑎 <s (𝐴 |s 𝐵))
135	52, 134	mp3an3 1479	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
136	133, 135	sylan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
137		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵))
138	136, 137	breqtrrd 5132	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑋)
139		rightval 28245	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (R‘𝑋) = {𝑧 ∈ (O‘(bday‘𝑋)) ∣ 𝑋 <s 𝑧}
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (R‘𝑋) = {𝑧 ∈ (O‘(bday‘𝑋)) ∣ 𝑋 <s 𝑧})
141	140	eleq2d 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ (R‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ (O‘(bday‘𝑋)) ∣ 𝑋 <s 𝑧}))
142		rabid 3432	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑧 ∈ (O‘(bday‘𝑋)) ∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ (O‘(bday‘𝑋)) ∧ 𝑋 <s 𝑧))
143	141, 142	bitrdi 290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ (R‘𝑋) ↔ (𝑧 ∈ (O‘(bday‘𝑋)) ∧ 𝑋 <s 𝑧)))
144	143	simplbda 505	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝑋 <s 𝑧)
145	144	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 <s 𝑧)
146	129, 130, 131, 138, 145	ltstrd 28129	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑧)
147	146	3adant3 1150	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑧)
148		velsn 4596	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {𝑧} ↔ 𝑏 = 𝑧)
149		breq2 5106	. . . . . . . . . . . . . . . . 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 28163	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝐴 <<s {𝑧})
154	153	anim1i 627	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ {𝑧} <<s 𝐵) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))
155	122, 123, 154	elrabd 3646	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
156		fnfvima 7243	. . . . . . . . . . 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 4922	. . . . . . . . . 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 3943	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ {𝑧} <<s 𝐵) → (bday‘(𝐴 |s 𝐵)) ⊆ (bday‘𝑧))
161	117, 160	mtand 828	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ¬ {𝑧} <<s 𝐵)
162	28	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ∈ V)
163	162, 125	jctil 529	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ∈ V ∧ 𝐵 ∈ V))
164	128	adantr 486	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} ⊆ No)
165	31	ad3antrrr 743	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ⊆ No)
166		simpr 490	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
167	164, 165, 166	3jca 1146	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤))
168		brslts 28157	. . . . . . . 8 ⊢ ({𝑧} <<s 𝐵 ↔ (({𝑧} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)))
169	163, 167, 168	sylanbrc 595	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} <<s 𝐵)
170	161, 169	mtand 828	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
171		rexnal 3114	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
172	170, 171	sylibr 237	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
173		vex 3454	. . . . . 6 ⊢ 𝑧 ∈ V
174		breq1 5105	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤))
175	174	ralbidv 3185	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
176	175	notbid 321	. . . . . 6 ⊢ (𝑡 = 𝑧 → (¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
177	173, 176	rexsn 4639	. . . . 5 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
178	172, 177	sylib 221	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
179	31	ad2antrr 739	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → 𝐵 ⊆ No)
180	179	sselda 3909	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No)
181	110	adantr 486	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ No)
182		lenlts 28118	. . . . . . 7 ⊢ ((𝑤 ∈ No ∧ 𝑧 ∈ No) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
183	180, 181, 182	syl2anc 596	. . . . . 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 290	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
187	178, 186	mpbird 260	. . 3 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ (R‘𝑋)) → ∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
188	187	ralrimiva 3154	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ (R‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
189	103, 188	jca 521	1 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ (L‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ (R‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086  {crab 3412  Vcvv 3450   ⊆ wss 3896  {csn 4584  ∩ cint 4906   class class class wbr 5102   “ cima 5654  Oncon0 6365   Fn wfn 6538  ‘cfv 6543  (class class class)co 7424  Nocsur 28006   <s clts 28007  bdaycbday 28008   ≤s cles 28110   <<s cslts 28152   |s ccuts 28154  Ocold 28218  Lcleft 28220  Rcright 28221

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6307  df-ord 6368  df-on 6369  df-suc 6371  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7381  df-ov 7427  df-oprab 7428  df-mpo 7429  df-2nd 8006  df-frecs 8307  df-wrecs 8338  df-recs 8387  df-1o 8484  df-2o 8485  df-no 28009  df-lts 28010  df-bday 28011  df-les 28111  df-slts 28153  df-cuts 28155  df-made 28222  df-old 28223  df-left 28225  df-right 28226

This theorem is used by:  cofcutr1d  28320  cofcutr2d  28321