Metamath Proof Explorer

Theorem conway

Description: Conway's Simplicity Theorem. Given A preceeding B , 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)

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

Proof

Step Hyp Ref Expression
1 sltsss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
2 sltsex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
3 sltsss2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
4 sltsex2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
5 sltssep ⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 )
6 noeta2 ⊢ ( ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 ) → ∃ 𝑦 ∈ No ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘ 𝑦 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
7 1 2 3 4 5 6 syl221anc ⊢ ( 𝐴 <<s 𝐵 → ∃ 𝑦 ∈ No ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘ 𝑦 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) )
8 3simpa ⊢ ( ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘ 𝑦 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) → ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) )
9 2 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → 𝐴 ∈ V )
10 vsnex ⊢ { 𝑦 } ∈ V
11 9 10 jctir ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → ( 𝐴 ∈ V ∧ { 𝑦 } ∈ V ) )
12 1 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → 𝐴 ⊆ No )
13 snssi ⊢ ( 𝑦 ∈ No → { 𝑦 } ⊆ No )
14 13 adantl ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → { 𝑦 } ⊆ No )
15 14 adantr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → { 𝑦 } ⊆ No )
16 vex ⊢ 𝑦 ∈ V
17 breq2 ⊢ ( 𝑞 = 𝑦 → ( 𝑝 <s 𝑞 ↔ 𝑝 <s 𝑦 ) )
18 16 17 ralsn ⊢ ( ∀ 𝑞 ∈ { 𝑦 } 𝑝 <s 𝑞 ↔ 𝑝 <s 𝑦 )
19 18 ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ { 𝑦 } 𝑝 <s 𝑞 ↔ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 )
20 19 biimpri ⊢ ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ { 𝑦 } 𝑝 <s 𝑞 )
21 20 adantl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ { 𝑦 } 𝑝 <s 𝑞 )
22 12 15 21 3jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → ( 𝐴 ⊆ No ∧ { 𝑦 } ⊆ No ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ { 𝑦 } 𝑝 <s 𝑞 ) )
23 brslts ⊢ ( 𝐴 <<s { 𝑦 } ↔ ( ( 𝐴 ∈ V ∧ { 𝑦 } ∈ V ) ∧ ( 𝐴 ⊆ No ∧ { 𝑦 } ⊆ No ∧ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ { 𝑦 } 𝑝 <s 𝑞 ) ) )
24 11 22 23 sylanbrc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ) → 𝐴 <<s { 𝑦 } )
25 24 ex ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 → 𝐴 <<s { 𝑦 } ) )
26 4 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → 𝐵 ∈ V )
27 26 10 jctil ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → ( { 𝑦 } ∈ V ∧ 𝐵 ∈ V ) )
28 14 adantr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → { 𝑦 } ⊆ No )
29 3 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → 𝐵 ⊆ No )
30 ralcom ⊢ ( ∀ 𝑝 ∈ { 𝑦 } ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 ↔ ∀ 𝑞 ∈ 𝐵 ∀ 𝑝 ∈ { 𝑦 } 𝑝 <s 𝑞 )
31 breq1 ⊢ ( 𝑝 = 𝑦 → ( 𝑝 <s 𝑞 ↔ 𝑦 <s 𝑞 ) )
32 16 31 ralsn ⊢ ( ∀ 𝑝 ∈ { 𝑦 } 𝑝 <s 𝑞 ↔ 𝑦 <s 𝑞 )
33 32 ralbii ⊢ ( ∀ 𝑞 ∈ 𝐵 ∀ 𝑝 ∈ { 𝑦 } 𝑝 <s 𝑞 ↔ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 )
34 30 33 sylbbr ⊢ ( ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 → ∀ 𝑝 ∈ { 𝑦 } ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 )
35 34 adantl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → ∀ 𝑝 ∈ { 𝑦 } ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 )
36 28 29 35 3jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → ( { 𝑦 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑝 ∈ { 𝑦 } ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 ) )
37 brslts ⊢ ( { 𝑦 } <<s 𝐵 ↔ ( ( { 𝑦 } ∈ V ∧ 𝐵 ∈ V ) ∧ ( { 𝑦 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑝 ∈ { 𝑦 } ∀ 𝑞 ∈ 𝐵 𝑝 <s 𝑞 ) ) )
38 27 36 37 sylanbrc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → { 𝑦 } <<s 𝐵 )
39 38 ex ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → ( ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 → { 𝑦 } <<s 𝐵 ) )
40 25 39 anim12d ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ) → ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ) )
41 8 40 syl5 ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘ 𝑦 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ) )
42 41 reximdva ⊢ ( 𝐴 <<s 𝐵 → ( ∃ 𝑦 ∈ No ( ∀ 𝑝 ∈ 𝐴 𝑝 <s 𝑦 ∧ ∀ 𝑞 ∈ 𝐵 𝑦 <s 𝑞 ∧ ( bday ‘ 𝑦 ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ) → ∃ 𝑦 ∈ No ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ) )
43 7 42 mpd ⊢ ( 𝐴 <<s 𝐵 → ∃ 𝑦 ∈ No ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) )
44 rabn0 ⊢ ( { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ≠ ∅ ↔ ∃ 𝑦 ∈ No ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) )
45 43 44 sylibr ⊢ ( 𝐴 <<s 𝐵 → { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ≠ ∅ )
46 ssrab2 ⊢ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No
47 46 a1i ⊢ ( 𝐴 <<s 𝐵 → { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No )
48 simplr3 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑟 ∈ No )
49 2 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐴 ∈ V )
50 vsnex ⊢ { 𝑟 } ∈ V
51 49 50 jctir ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( 𝐴 ∈ V ∧ { 𝑟 } ∈ V ) )
52 1 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐴 ⊆ No )
53 48 snssd ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → { 𝑟 } ⊆ No )
54 52 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
55 simplr1 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑝 ∈ No )
56 55 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑝 ∈ No )
57 48 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑟 ∈ No )
58 simplll ⊢ ( ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) → 𝐴 <<s { 𝑝 } )
59 58 adantl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐴 <<s { 𝑝 } )
60 sltssep ⊢ ( 𝐴 <<s { 𝑝 } → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 )
61 59 60 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 )
62 61 r19.21bi ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 )
63 vex ⊢ 𝑝 ∈ V
64 breq2 ⊢ ( 𝑦 = 𝑝 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝 ) )
65 63 64 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝 )
66 62 65 sylib ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 <s 𝑝 )
67 simprrl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑝 <s 𝑟 )
68 67 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑝 <s 𝑟 )
69 54 56 57 66 68 ltstrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 <s 𝑟 )
70 vex ⊢ 𝑟 ∈ V
71 breq2 ⊢ ( 𝑦 = 𝑟 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟 ) )
72 70 71 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟 )
73 69 72 sylibr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 )
74 73 ralrimiva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 )
75 52 53 74 3jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( 𝐴 ⊆ No ∧ { 𝑟 } ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 ) )
76 brslts ⊢ ( 𝐴 <<s { 𝑟 } ↔ ( ( 𝐴 ∈ V ∧ { 𝑟 } ∈ V ) ∧ ( 𝐴 ⊆ No ∧ { 𝑟 } ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 ) ) )
77 51 75 76 sylanbrc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐴 <<s { 𝑟 } )
78 4 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐵 ∈ V )
79 78 50 jctil ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( { 𝑟 } ∈ V ∧ 𝐵 ∈ V ) )
80 3 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐵 ⊆ No )
81 48 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 ∈ No )
82 simplr2 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑞 ∈ No )
83 82 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑞 ∈ No )
84 80 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ No )
85 simprrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑟 <s 𝑞 )
86 85 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 <s 𝑞 )
87 simplrr ⊢ ( ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) → { 𝑞 } <<s 𝐵 )
88 87 adantl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → { 𝑞 } <<s 𝐵 )
89 sltssep ⊢ ( { 𝑞 } <<s 𝐵 → ∀ 𝑥 ∈ { 𝑞 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
90 88 89 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ { 𝑞 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
91 vex ⊢ 𝑞 ∈ V
92 breq1 ⊢ ( 𝑥 = 𝑞 → ( 𝑥 <s 𝑦 ↔ 𝑞 <s 𝑦 ) )
93 92 ralbidv ⊢ ( 𝑥 = 𝑞 → ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑞 <s 𝑦 ) )
94 91 93 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝑞 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑞 <s 𝑦 )
95 90 94 sylib ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑦 ∈ 𝐵 𝑞 <s 𝑦 )
96 95 r19.21bi ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑞 <s 𝑦 )
97 81 83 84 86 96 ltstrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 <s 𝑦 )
98 97 ralrimiva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑦 ∈ 𝐵 𝑟 <s 𝑦 )
99 breq1 ⊢ ( 𝑥 = 𝑟 → ( 𝑥 <s 𝑦 ↔ 𝑟 <s 𝑦 ) )
100 99 ralbidv ⊢ ( 𝑥 = 𝑟 → ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑟 <s 𝑦 ) )
101 70 100 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑟 <s 𝑦 )
102 98 101 sylibr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
103 53 80 102 3jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( { 𝑟 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
104 brslts ⊢ ( { 𝑟 } <<s 𝐵 ↔ ( ( { 𝑟 } ∈ V ∧ 𝐵 ∈ V ) ∧ ( { 𝑟 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )
105 79 103 104 sylanbrc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → { 𝑟 } <<s 𝐵 )
106 48 77 105 jca32 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) )
107 106 exp44 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) → ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
108 107 ralrimivvva ⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
109 sneq ⊢ ( 𝑦 = 𝑝 → { 𝑦 } = { 𝑝 } )
110 109 breq2d ⊢ ( 𝑦 = 𝑝 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑝 } ) )
111 109 breq1d ⊢ ( 𝑦 = 𝑝 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑝 } <<s 𝐵 ) )
112 110 111 anbi12d ⊢ ( 𝑦 = 𝑝 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ) )
113 112 ralrab ⊢ ( ∀ 𝑝 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ↔ ∀ 𝑝 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
114 sneq ⊢ ( 𝑦 = 𝑞 → { 𝑦 } = { 𝑞 } )
115 114 breq2d ⊢ ( 𝑦 = 𝑞 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑞 } ) )
116 114 breq1d ⊢ ( 𝑦 = 𝑞 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑞 } <<s 𝐵 ) )
117 115 116 anbi12d ⊢ ( 𝑦 = 𝑞 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) )
118 117 ralrab ⊢ ( ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ↔ ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
119 sneq ⊢ ( 𝑦 = 𝑟 → { 𝑦 } = { 𝑟 } )
120 119 breq2d ⊢ ( 𝑦 = 𝑟 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑟 } ) )
121 119 breq1d ⊢ ( 𝑦 = 𝑟 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑟 } <<s 𝐵 ) )
122 120 121 anbi12d ⊢ ( 𝑦 = 𝑟 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) )
123 122 elrab ⊢ ( 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) )
124 123 imbi2i ⊢ ( ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) )
125 124 ralbii ⊢ ( ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) )
126 125 ralbii ⊢ ( ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) )
127 r19.21v ⊢ ( ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
128 127 ralbii ⊢ ( ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ↔ ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
129 118 126 128 3bitr4i ⊢ ( ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
130 129 ralbii ⊢ ( ∀ 𝑝 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑝 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
131 r19.21v ⊢ ( ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
132 131 ralbii ⊢ ( ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
133 r19.21v ⊢ ( ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
134 132 133 bitri ⊢ ( ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
135 134 ralbii ⊢ ( ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ∀ 𝑝 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
136 113 130 135 3bitr4i ⊢ ( ∀ 𝑝 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
137 108 136 sylibr ⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑝 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
138 nocvxmin ⊢ ( ( { 𝑦 ∈ 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 𝐵 ) } ) )
139 45 47 137 138 syl3anc ⊢ ( 𝐴 <<s 𝐵 → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )