Theorem cofcutr 33747

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		bdayelon 33626	. . . . . . . . . 10 ⊢ ( bday ‘(𝐴 |s 𝐵)) ∈ On
2	1	onssneli 6292	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥) → ¬ ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
3		leftssold 33716	. . . . . . . . . . . . 13 ⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
4	3	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
5	4	sselda 3887	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ ( O ‘( bday ‘𝑋)))
6		bdayelon 33626	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑋) ∈ On
7		leftssno 33718	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑋) ⊆ No
8	7	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) ⊆ No )
9	8	sselda 3887	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑥 ∈ No )
10		oldbday 33736	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑥 ∈ No ) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
11	6, 9, 10	sylancr 590	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (𝑥 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑥) ∈ ( bday ‘𝑋)))
12	5, 11	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘𝑋))
13		simplr 769	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
14	13	fveq2d 6690	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
15	12, 14	eleqtrd 2836	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ( bday ‘𝑥) ∈ ( bday ‘(𝐴 |s 𝐵)))
16	2, 15	nsyl3 140	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
17		scutbday 33653	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
18	17	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
19		bdayfn 33623	. . . . . . . . . . 11 ⊢ bday Fn No
20		ssrab2 3979	. . . . . . . . . . 11 ⊢ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No
21		sneq 4536	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑥 → {𝑡} = {𝑥})
22	21	breq2d 5052	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑥}))
23	21	breq1d 5050	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → ({𝑡} <<s 𝐵 ↔ {𝑥} <<s 𝐵))
24	22, 23	anbi12d 634	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
25	9	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ No )
26		snex 5308	. . . . . . . . . . . . . . 15 ⊢ {𝑥} ∈ V
27	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ∈ V)
28		ssltex2 33637	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
29	28	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐵 ∈ V)
30	9	snssd 4707	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} ⊆ No )
31		ssltss2 33639	. . . . . . . . . . . . . . 15 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
32	31	ad2antrr 726	. . . . . . . . . . . . . 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	scutcld 33652	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝐴 |s 𝐵) ∈ No )
37	34, 36	eqeltrd 2834	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → 𝑋 ∈ No )
38	37	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 ∈ No )
39	32	sselda 3887	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ No )
40		leftval 33702	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}
41	40	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋})
42	41	eleq2d 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋}))
43		rabid 3282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))
44	42, 43	bitrdi 290	. . . . . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 = (𝐴 |s 𝐵))
48		scutcut 33650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 <<s 𝐵 → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
49	48	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
50	49	simp3d 1145	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {(𝐴 |s 𝐵)} <<s 𝐵)
51		ovex 7215	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 |s 𝐵) ∈ V
52	51	snid 4562	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}
53		ssltsepc 33642	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)} ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
54	52, 53	mp3an2 1450	. . . . . . . . . . . . . . . . . . 19 ⊢ (({(𝐴 |s 𝐵)} <<s 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
55	50, 54	sylan 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → (𝐴 |s 𝐵) <s 𝑏)
56	47, 55	eqbrtrd 5062	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑋 <s 𝑏)
57	33, 38, 39, 46, 56	slttrd 33617	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
58	57	3adant2 1132	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑥 <s 𝑏)
59		velsn 4542	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ {𝑥} ↔ 𝑎 = 𝑥)
60		breq1 5043	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
61	59, 60	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ∈ {𝑥} → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
62	61	3ad2ant2 1135	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → (𝑎 <s 𝑏 ↔ 𝑥 <s 𝑏))
63	58, 62	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑎 ∈ {𝑥} ∧ 𝑏 ∈ 𝐵) → 𝑎 <s 𝑏)
64	27, 29, 30, 32, 63	ssltd 33641	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → {𝑥} <<s 𝐵)
65	64	anim1ci 619	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))
66	24, 25, 65	elrabd 3595	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
67		fnfvima 7018	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑥 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
68	19, 20, 66, 67	mp3an12i 1466	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘𝑥) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
69		intss1 4861	. . . . . . . . . 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 3925	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝐴 <<s {𝑥}) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑥))
72	16, 71	mtand 816	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ 𝐴 <<s {𝑥})
73		ssltex1 33636	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
74	73	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ∈ V)
75	74, 26	jctir 524	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ∈ V ∧ {𝑥} ∈ V))
76		ssltss1 33638	. . . . . . . . . 10 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
77	76	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 ⊆ No )
78	9	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝑥 ∈ No )
79	78	snssd 4707	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → {𝑥} ⊆ No )
80		simpr 488	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
81	77, 79, 80	3jca 1129	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡))
82		brsslt 33635	. . . . . . . 8 ⊢ (𝐴 <<s {𝑥} ↔ ((𝐴 ∈ V ∧ {𝑥} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑥} ⊆ No ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)))
83	75, 81, 82	sylanbrc 586	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡) → 𝐴 <<s {𝑥})
84	72, 83	mtand 816	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
85		rexnal 3152	. . . . . . 7 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
86		ralcom 3259	. . . . . . 7 ⊢ (∀𝑡 ∈ {𝑥}∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
87	85, 86	xchbinx 337	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 ∀𝑡 ∈ {𝑥}𝑦 <s 𝑡)
88	84, 87	sylibr 237	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡)
89		vex 3404	. . . . . 6 ⊢ 𝑥 ∈ V
90		breq2 5044	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (𝑦 <s 𝑡 ↔ 𝑦 <s 𝑥))
91	90	ralbidv 3110	. . . . . . 7 ⊢ (𝑡 = 𝑥 → (∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
92	91	notbid 321	. . . . . 6 ⊢ (𝑡 = 𝑥 → (¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥))
93	89, 92	rexsn 4583	. . . . 5 ⊢ (∃𝑡 ∈ {𝑥} ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑡 ↔ ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
94	88, 93	sylib 221	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → ¬ ∀𝑦 ∈ 𝐴 𝑦 <s 𝑥)
95	76	ad2antrr 726	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → 𝐴 ⊆ No )
96	95	sselda 3887	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ No )
97		slenlt 33610	. . . . . . 7 ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
98	9, 96, 97	syl2an2r 685	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) ∧ 𝑦 ∈ 𝐴) → (𝑥 ≤s 𝑦 ↔ ¬ 𝑦 <s 𝑥))
99	98	rexbidva 3207	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑥 ∈ ( L ‘𝑋)) → (∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ↔ ∃𝑦 ∈ 𝐴 ¬ 𝑦 <s 𝑥))
100		rexnal 3152	. . . . 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 3097	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦)
104	1	onssneli 6292	. . . . . . . . 9 ⊢ (( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧) → ¬ ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
105		rightssold 33717	. . . . . . . . . . . . 13 ⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
106	105	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋)))
107	106	sselda 3887	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ ( O ‘( bday ‘𝑋)))
108		rightssno 33719	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝑋) ⊆ No
109	108	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) ⊆ No )
110	109	sselda 3887	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑧 ∈ No )
111		oldbday 33736	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑧 ∈ No ) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
112	6, 110, 111	sylancr 590	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (𝑧 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑧) ∈ ( bday ‘𝑋)))
113	107, 112	mpbid 235	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘𝑋))
114		simplr 769	. . . . . . . . . . 11 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝑋 = (𝐴 |s 𝐵))
115	114	fveq2d 6690	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑋) = ( bday ‘(𝐴 |s 𝐵)))
116	113, 115	eleqtrd 2836	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ( bday ‘𝑧) ∈ ( bday ‘(𝐴 |s 𝐵)))
117	104, 116	nsyl3 140	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
118	17	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) = ∩ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
119		sneq 4536	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → {𝑡} = {𝑧})
120	119	breq2d 5052	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (𝐴 <<s {𝑡} ↔ 𝐴 <<s {𝑧}))
121	119	breq1d 5050	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → ({𝑡} <<s 𝐵 ↔ {𝑧} <<s 𝐵))
122	120, 121	anbi12d 634	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑧 → ((𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵) ↔ (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵)))
123	110	adantr 484	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ No )
124	73	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ∈ V)
125		snex 5308	. . . . . . . . . . . . . . 15 ⊢ {𝑧} ∈ V
126	125	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ∈ V)
127	76	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 ⊆ No )
128	110	snssd 4707	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → {𝑧} ⊆ No )
129	127	sselda 3887	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ No )
130	37	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 ∈ No )
131	110	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑧 ∈ No )
132	48	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ((𝐴 |s 𝐵) ∈ No ∧ 𝐴 <<s {(𝐴 |s 𝐵)} ∧ {(𝐴 |s 𝐵)} <<s 𝐵))
133	132	simp2d 1144	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {(𝐴 |s 𝐵)})
134		ssltsepc 33642	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴 ∧ (𝐴 |s 𝐵) ∈ {(𝐴 |s 𝐵)}) → 𝑎 <s (𝐴 |s 𝐵))
135	52, 134	mp3an3 1451	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 <<s {(𝐴 |s 𝐵)} ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
136	133, 135	sylan 583	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s (𝐴 |s 𝐵))
137		simpllr 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑋 = (𝐴 |s 𝐵))
138	136, 137	breqtrrd 5068	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑋)
139		rightval 33703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}
140	139	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ( R ‘𝑋) = {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧})
141	140	eleq2d 2819	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (𝑧 ∈ ( R ‘𝑋) ↔ 𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧}))
142		rabid 3282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑧 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑧} ↔ (𝑧 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑧))
143	141, 142	bitrdi 290	. . . . . . . . . . . . . . . . . . 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	slttrd 33617	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴) → 𝑎 <s 𝑧)
147	146	3adant3 1133	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑧)
148		velsn 4542	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ {𝑧} ↔ 𝑏 = 𝑧)
149		breq2 5044	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝑧 → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
150	148, 149	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ {𝑧} → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
151	150	3ad2ant3 1136	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → (𝑎 <s 𝑏 ↔ 𝑎 <s 𝑧))
152	147, 151	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ {𝑧}) → 𝑎 <s 𝑏)
153	124, 126, 127, 128, 152	ssltd 33641	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐴 <<s {𝑧})
154	153	anim1i 618	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → (𝐴 <<s {𝑧} ∧ {𝑧} <<s 𝐵))
155	122, 123, 154	elrabd 3595	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)})
156		fnfvima 7018	. . . . . . . . . . 11 ⊢ (( bday Fn No ∧ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)} ⊆ No ∧ 𝑧 ∈ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
157	19, 20, 155, 156	mp3an12i 1466	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘𝑧) ∈ ( bday “ {𝑡 ∈ No ∣ (𝐴 <<s {𝑡} ∧ {𝑡} <<s 𝐵)}))
158		intss1 4861	. . . . . . . . . 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 3925	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ {𝑧} <<s 𝐵) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday ‘𝑧))
161	117, 160	mtand 816	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ {𝑧} <<s 𝐵)
162	28	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ∈ V)
163	162, 125	jctil 523	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ∈ V ∧ 𝐵 ∈ V))
164	128	adantr 484	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} ⊆ No )
165	31	ad3antrrr 730	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → 𝐵 ⊆ No )
166		simpr 488	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
167	164, 165, 166	3jca 1129	. . . . . . . 8 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤))
168		brsslt 33635	. . . . . . . 8 ⊢ ({𝑧} <<s 𝐵 ↔ (({𝑧} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑧} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)))
169	163, 167, 168	sylanbrc 586	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤) → {𝑧} <<s 𝐵)
170	161, 169	mtand 816	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
171		rexnal 3152	. . . . . 6 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑡 ∈ {𝑧}∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
172	170, 171	sylibr 237	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤)
173		vex 3404	. . . . . 6 ⊢ 𝑧 ∈ V
174		breq1 5043	. . . . . . . 8 ⊢ (𝑡 = 𝑧 → (𝑡 <s 𝑤 ↔ 𝑧 <s 𝑤))
175	174	ralbidv 3110	. . . . . . 7 ⊢ (𝑡 = 𝑧 → (∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
176	175	notbid 321	. . . . . 6 ⊢ (𝑡 = 𝑧 → (¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤))
177	173, 176	rexsn 4583	. . . . 5 ⊢ (∃𝑡 ∈ {𝑧} ¬ ∀𝑤 ∈ 𝐵 𝑡 <s 𝑤 ↔ ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
178	172, 177	sylib 221	. . . 4 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → ¬ ∀𝑤 ∈ 𝐵 𝑧 <s 𝑤)
179	31	ad2antrr 726	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → 𝐵 ⊆ No )
180	179	sselda 3887	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈ No )
181	110	adantr 484	. . . . . . 7 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → 𝑧 ∈ No )
182		slenlt 33610	. . . . . . 7 ⊢ ((𝑤 ∈ No ∧ 𝑧 ∈ No ) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
183	180, 181, 182	syl2anc 587	. . . . . 6 ⊢ ((((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) ∧ 𝑤 ∈ 𝐵) → (𝑤 ≤s 𝑧 ↔ ¬ 𝑧 <s 𝑤))
184	183	rexbidva 3207	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) ∧ 𝑧 ∈ ( R ‘𝑋)) → (∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧 ↔ ∃𝑤 ∈ 𝐵 ¬ 𝑧 <s 𝑤))
185		rexnal 3152	. . . . 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 3097	. 2 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧)
189	103, 188	jca 515	1 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑋 = (𝐴 |s 𝐵)) → (∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦 ∧ ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1088   = wceq 1542   ∈ wcel 2114  ∀wral 3054  ∃wrex 3055  {crab 3058  Vcvv 3400   ⊆ wss 3853  {csn 4526  ∩ cint 4846   class class class wbr 5040   “ cima 5538  Oncon0 6182   Fn wfn 6344  ‘cfv 6349  (class class class)co 7182   No csur 33498   <s cslt 33499   bday cbday 33500   ≤s csle 33602   <<s csslt 33630   |s cscut 33632   O cold 33682   L cleft 33684   R cright 33685

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5242  ax-pr 5306  ax-un 7491

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3402  df-sbc 3686  df-csb 3801  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4222  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4807  df-int 4847  df-iun 4893  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5439  df-eprel 5444  df-po 5452  df-so 5453  df-fr 5493  df-we 5495  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548  df-pred 6139  df-ord 6185  df-on 6186  df-suc 6188  df-iota 6307  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7139  df-ov 7185  df-oprab 7186  df-mpo 7187  df-wrecs 7988  df-recs 8049  df-1o 8143  df-2o 8144  df-no 33501  df-slt 33502  df-bday 33503  df-sle 33603  df-sslt 33631  df-scut 33633  df-made 33686  df-old 33687  df-left 33689  df-right 33690

This theorem is referenced by: (None)