Theorem conway 27930

Description: Conway's Simplicity Theorem. Given 𝐴 preceeding 𝐵, there is a unique surreal of minimal length separating them. This is a fundamental property of surreals and will be used (via surreal cuts) to prove many properties later on. Theorem from [Alling] p. 185. (Contributed by Scott Fenton, 8-Dec-2021.)

Assertion

Ref	Expression
conway	⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))

Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem conway

Dummy variables 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sltsss1 27916	. . . . 5 ⊢ (𝐴 <<s 𝐵 → 𝐴 ⊆ No )
2		sltsex1 27914	. . . . 5 ⊢ (𝐴 <<s 𝐵 → 𝐴 ∈ V)
3		sltsss2 27917	. . . . 5 ⊢ (𝐴 <<s 𝐵 → 𝐵 ⊆ No )
4		sltsex2 27915	. . . . 5 ⊢ (𝐴 <<s 𝐵 → 𝐵 ∈ V)
5		sltssep 27918	. . . . 5 ⊢ (𝐴 <<s 𝐵 → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐵 𝑝 <s 𝑞)
6		noeta2 27912	. . . . 5 ⊢ (((𝐴 ⊆ No ∧ 𝐴 ∈ V) ∧ (𝐵 ⊆ No ∧ 𝐵 ∈ V) ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐵 𝑝 <s 𝑞) → ∃𝑦 ∈ No (∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘𝑦) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
7	1, 2, 3, 4, 5, 6	syl221anc 1404	. . . 4 ⊢ (𝐴 <<s 𝐵 → ∃𝑦 ∈ No (∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘𝑦) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))))
8		3simpa 1164	. . . . . 6 ⊢ ((∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘𝑦) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) → (∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞))
9	2	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → 𝐴 ∈ V)
10		vsnex 5397	. . . . . . . . . 10 ⊢ {𝑦} ∈ V
11	9, 10	jctir 529	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → (𝐴 ∈ V ∧ {𝑦} ∈ V))
12	1	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → 𝐴 ⊆ No )
13		snssi 4747	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ No → {𝑦} ⊆ No )
14	13	adantl 486	. . . . . . . . . . 11 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → {𝑦} ⊆ No )
15	14	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → {𝑦} ⊆ No )
16		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑦 ∈ V
17		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑦 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑦))
18	16, 17	ralsn 4643	. . . . . . . . . . . 12 ⊢ (∀𝑞 ∈ {𝑦}𝑝 <s 𝑞 ↔ 𝑝 <s 𝑦)
19	18	ralbii 3111	. . . . . . . . . . 11 ⊢ (∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞 ↔ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦)
20	19	bilanri 511	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞)
21	12, 15, 20	3jca 1144	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → (𝐴 ⊆ No ∧ {𝑦} ⊆ No ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞))
22		brslts 27913	. . . . . . . . 9 ⊢ (𝐴 <<s {𝑦} ↔ ((𝐴 ∈ V ∧ {𝑦} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑦} ⊆ No ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ {𝑦}𝑝 <s 𝑞)))
23	11, 21, 22	sylanbrc 594	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑝 ∈ 𝐴 𝑝 <s 𝑦) → 𝐴 <<s {𝑦})
24	23	ex 417	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → (∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 → 𝐴 <<s {𝑦}))
25	4	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → 𝐵 ∈ V)
26	25, 10	jctil 528	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → ({𝑦} ∈ V ∧ 𝐵 ∈ V))
27	14	adantr 485	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → {𝑦} ⊆ No )
28	3	ad2antrr 738	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → 𝐵 ⊆ No )
29		ralcom 3293	. . . . . . . . . . . 12 ⊢ (∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞 ↔ ∀𝑞 ∈ 𝐵 ∀𝑝 ∈ {𝑦}𝑝 <s 𝑞)
30		breq1 5108	. . . . . . . . . . . . . 14 ⊢ (𝑝 = 𝑦 → (𝑝 <s 𝑞 ↔ 𝑦 <s 𝑞))
31	16, 30	ralsn 4643	. . . . . . . . . . . . 13 ⊢ (∀𝑝 ∈ {𝑦}𝑝 <s 𝑞 ↔ 𝑦 <s 𝑞)
32	31	ralbii 3111	. . . . . . . . . . . 12 ⊢ (∀𝑞 ∈ 𝐵 ∀𝑝 ∈ {𝑦}𝑝 <s 𝑞 ↔ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞)
33	29, 32	sylbbr 239	. . . . . . . . . . 11 ⊢ (∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 → ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞)
34	33	adantl 486	. . . . . . . . . 10 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞)
35	27, 28, 34	3jca 1144	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → ({𝑦} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞))
36		brslts 27913	. . . . . . . . 9 ⊢ ({𝑦} <<s 𝐵 ↔ (({𝑦} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑦} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑝 ∈ {𝑦}∀𝑞 ∈ 𝐵 𝑝 <s 𝑞)))
37	26, 35, 36	sylanbrc 594	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → {𝑦} <<s 𝐵)
38	37	ex 417	. . . . . . 7 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → (∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 → {𝑦} <<s 𝐵))
39	24, 38	anim12d 620	. . . . . 6 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → ((∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞) → (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)))
40	8, 39	syl5 35	. . . . 5 ⊢ ((𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → ((∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘𝑦) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) → (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)))
41	40	reximdva 3178	. . . 4 ⊢ (𝐴 <<s 𝐵 → (∃𝑦 ∈ No (∀𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘𝑦) ⊆ suc ∪ ( bday “ (𝐴 ∪ 𝐵))) → ∃𝑦 ∈ No (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)))
42	7, 41	mpd 16	. . 3 ⊢ (𝐴 <<s 𝐵 → ∃𝑦 ∈ No (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))
43		rabn0 4346	. . 3 ⊢ ({𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ≠ ∅ ↔ ∃𝑦 ∈ No (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵))
44	42, 43	sylibr 237	. 2 ⊢ (𝐴 <<s 𝐵 → {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ≠ ∅)
45		ssrab2 4036	. . 3 ⊢ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
46	45	a1i 11	. 2 ⊢ (𝐴 <<s 𝐵 → {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No )
47		simplr3 1234	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑟 ∈ No )
48	2	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 ∈ V)
49		vsnex 5397	. . . . . . . 8 ⊢ {𝑟} ∈ V
50	48, 49	jctir 529	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → (𝐴 ∈ V ∧ {𝑟} ∈ V))
51	1	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 ⊆ No )
52	47	snssd 4748	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → {𝑟} ⊆ No )
53	51	sselda 3939	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ No )
54		simplr1 1232	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑝 ∈ No )
55	54	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑝 ∈ No )
56	47	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑟 ∈ No )
57		simplll 786	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞)) → 𝐴 <<s {𝑝})
58	57	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 <<s {𝑝})
59		sltssep 27918	. . . . . . . . . . . . . 14 ⊢ (𝐴 <<s {𝑝} → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑝}𝑥 <s 𝑦)
60	58, 59	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑝}𝑥 <s 𝑦)
61	60	r19.21bi 3257	. . . . . . . . . . . 12 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑝}𝑥 <s 𝑦)
62		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑝 ∈ V
63		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑝 → (𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝))
64	62, 63	ralsn 4643	. . . . . . . . . . . 12 ⊢ (∀𝑦 ∈ {𝑝}𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝)
65	61, 64	sylib 221	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s 𝑝)
66		simprrl 792	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑝 <s 𝑟)
67	66	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑝 <s 𝑟)
68	53, 55, 56, 65, 67	ltstrd 27885	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → 𝑥 <s 𝑟)
69		vex 3461	. . . . . . . . . . 11 ⊢ 𝑟 ∈ V
70		breq2 5109	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟))
71	69, 70	ralsn 4643	. . . . . . . . . 10 ⊢ (∀𝑦 ∈ {𝑟}𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟)
72	68, 71	sylibr 237	. . . . . . . . 9 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦)
73	72	ralrimiva 3157	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦)
74	51, 52, 73	3jca 1144	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → (𝐴 ⊆ No ∧ {𝑟} ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦))
75		brslts 27913	. . . . . . 7 ⊢ (𝐴 <<s {𝑟} ↔ ((𝐴 ∈ V ∧ {𝑟} ∈ V) ∧ (𝐴 ⊆ No ∧ {𝑟} ⊆ No ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ {𝑟}𝑥 <s 𝑦)))
76	50, 74, 75	sylanbrc 594	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐴 <<s {𝑟})
77	4	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐵 ∈ V)
78	77, 49	jctil 528	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ({𝑟} ∈ V ∧ 𝐵 ∈ V))
79	3	ad2antrr 738	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝐵 ⊆ No )
80	47	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑟 ∈ No )
81		simplr2 1233	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑞 ∈ No )
82	81	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑞 ∈ No )
83	79	sselda 3939	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ No )
84		simprrr 793	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → 𝑟 <s 𝑞)
85	84	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑟 <s 𝑞)
86		simplrr 789	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞)) → {𝑞} <<s 𝐵)
87	86	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → {𝑞} <<s 𝐵)
88		sltssep 27918	. . . . . . . . . . . . . 14 ⊢ ({𝑞} <<s 𝐵 → ∀𝑥 ∈ {𝑞}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
89	87, 88	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ {𝑞}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
90		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑞 ∈ V
91		breq1 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑞 → (𝑥 <s 𝑦 ↔ 𝑞 <s 𝑦))
92	91	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑞 → (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑞 <s 𝑦))
93	90, 92	ralsn 4643	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ {𝑞}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑞 <s 𝑦)
94	89, 93	sylib 221	. . . . . . . . . . . 12 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑦 ∈ 𝐵 𝑞 <s 𝑦)
95	94	r19.21bi 3257	. . . . . . . . . . 11 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑞 <s 𝑦)
96	80, 82, 83, 85, 95	ltstrd 27885	. . . . . . . . . 10 ⊢ ((((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) ∧ 𝑦 ∈ 𝐵) → 𝑟 <s 𝑦)
97	96	ralrimiva 3157	. . . . . . . . 9 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑦 ∈ 𝐵 𝑟 <s 𝑦)
98		breq1 5108	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑟 → (𝑥 <s 𝑦 ↔ 𝑟 <s 𝑦))
99	98	ralbidv 3188	. . . . . . . . . 10 ⊢ (𝑥 = 𝑟 → (∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑟 <s 𝑦))
100	69, 99	ralsn 4643	. . . . . . . . 9 ⊢ (∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑟 <s 𝑦)
101	97, 100	sylibr 237	. . . . . . . 8 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)
102	52, 79, 101	3jca 1144	. . . . . . 7 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → ({𝑟} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦))
103		brslts 27913	. . . . . . 7 ⊢ ({𝑟} <<s 𝐵 ↔ (({𝑟} ∈ V ∧ 𝐵 ∈ V) ∧ ({𝑟} ⊆ No ∧ 𝐵 ⊆ No ∧ ∀𝑥 ∈ {𝑟}∀𝑦 ∈ 𝐵 𝑥 <s 𝑦)))
104	78, 102, 103	sylanbrc 594	. . . . . 6 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → {𝑟} <<s 𝐵)
105	47, 76, 104	jca32 524	. . . . 5 ⊢ (((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) ∧ (((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) ∧ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)) ∧ (𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞))) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))
106	105	exp44 442	. . . 4 ⊢ ((𝐴 <<s 𝐵 ∧ (𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No )) → ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
107	106	ralrimivvva 3211	. . 3 ⊢ (𝐴 <<s 𝐵 → ∀𝑝 ∈ No ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
108		sneq 4595	. . . . . . 7 ⊢ (𝑦 = 𝑝 → {𝑦} = {𝑝})
109	108	breq2d 5117	. . . . . 6 ⊢ (𝑦 = 𝑝 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑝}))
110	108	breq1d 5115	. . . . . 6 ⊢ (𝑦 = 𝑝 → ({𝑦} <<s 𝐵 ↔ {𝑝} <<s 𝐵))
111	109, 110	anbi12d 643	. . . . 5 ⊢ (𝑦 = 𝑝 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵)))
112	111	ralrab 3660	. . . 4 ⊢ (∀𝑝 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) ↔ ∀𝑝 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
113		sneq 4595	. . . . . . . . 9 ⊢ (𝑦 = 𝑞 → {𝑦} = {𝑞})
114	113	breq2d 5117	. . . . . . . 8 ⊢ (𝑦 = 𝑞 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑞}))
115	113	breq1d 5115	. . . . . . . 8 ⊢ (𝑦 = 𝑞 → ({𝑦} <<s 𝐵 ↔ {𝑞} <<s 𝐵))
116	114, 115	anbi12d 643	. . . . . . 7 ⊢ (𝑦 = 𝑞 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵)))
117	116	ralrab 3660	. . . . . 6 ⊢ (∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))) ↔ ∀𝑞 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))
118		sneq 4595	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑟 → {𝑦} = {𝑟})
119	118	breq2d 5117	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑟}))
120	118	breq1d 5115	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑟 → ({𝑦} <<s 𝐵 ↔ {𝑟} <<s 𝐵))
121	119, 120	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑦 = 𝑟 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))
122	121	elrab 3653	. . . . . . . . 9 ⊢ (𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))
123	122	imbi2i 339	. . . . . . . 8 ⊢ (((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))
124	123	ralbii 3111	. . . . . . 7 ⊢ (∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))
125	124	ralbii 3111	. . . . . 6 ⊢ (∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))
126		r19.21v 3190	. . . . . . 7 ⊢ (∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) ↔ ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))
127	126	ralbii 3111	. . . . . 6 ⊢ (∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))) ↔ ∀𝑞 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))
128	117, 125, 127	3bitr4i 306	. . . . 5 ⊢ (∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))
129	128	ralbii 3111	. . . 4 ⊢ (∀𝑝 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑝 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵)))))
130		r19.21v 3190	. . . . . . 7 ⊢ (∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
131	130	ralbii 3111	. . . . . 6 ⊢ (∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ∀𝑞 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
132		r19.21v 3190	. . . . . 6 ⊢ (∀𝑞 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
133	131, 132	bitri 278	. . . . 5 ⊢ (∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
134	133	ralbii 3111	. . . 4 ⊢ (∀𝑝 ∈ No ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))) ↔ ∀𝑝 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
135	112, 129, 134	3bitr4i 306	. . 3 ⊢ (∀𝑝 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ↔ ∀𝑝 ∈ No ∀𝑞 ∈ No ∀𝑟 ∈ No ((𝐴 <<s {𝑝} ∧ {𝑝} <<s 𝐵) → ((𝐴 <<s {𝑞} ∧ {𝑞} <<s 𝐵) → ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → (𝑟 ∈ No ∧ (𝐴 <<s {𝑟} ∧ {𝑟} <<s 𝐵))))))
136	107, 135	sylibr 237	. 2 ⊢ (𝐴 <<s 𝐵 → ∀𝑝 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
137		nocvxmin 27906	. 2 ⊢ (({𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ≠ ∅ ∧ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No ∧ ∀𝑝 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑞 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}∀𝑟 ∈ No ((𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞) → 𝑟 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})) → ∃!𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
138	44, 46, 136, 137	syl3anc 1394	1 ⊢ (𝐴 <<s 𝐵 → ∃!𝑥 ∈ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ( bday ‘𝑥) = ∩ ( bday “ {𝑦 ∈ No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145   ≠ wne 2960  ∀wral 3079  ∃wrex 3089  ∃!wreu 3368  {crab 3417  Vcvv 3457   ∪ cun 3905   ⊆ wss 3907  ∅c0 4288  {csn 4585  ∪ cuni 4868  ∩ cint 4908   class class class wbr 5105   “ cima 5655  suc csuc 6352  ‘cfv 6525   No csur 27762   <s clts 27763   bday cbday 27764   <<s cslts 27908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rmo 3370  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4869  df-int 4909  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-ord 6353  df-on 6354  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-1o 8441  df-2o 8442  df-no 27765  df-lts 27766  df-bday 27767  df-slts 27909

This theorem is referenced by:  cutcuts  27932  cutbday  27935  eqcuts  27936  cutsun12  27941  cutbdaylt  27949