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