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 ssltss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
2 ssltex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
3 ssltss2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
4 ssltex2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
5 ssltsep ⊢ ( 𝐴 <<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 snex ⊢ { 𝑦 } ∈ 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 brsslt ⊢ ( 𝐴 <<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 brsslt ⊢ ( { 𝑦 } <<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 snex ⊢ { 𝑟 } ∈ 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 snssi ⊢ ( 𝑟 ∈ No → { 𝑟 } ⊆ No )
54 48 53 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → { 𝑟 } ⊆ No )
55 52 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
56 simplr1 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑝 ∈ No )
57 56 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑝 ∈ No )
58 48 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑟 ∈ No )
59 simplll ⊢ ( ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) → 𝐴 <<s { 𝑝 } )
60 59 adantl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐴 <<s { 𝑝 } )
61 ssltsep ⊢ ( 𝐴 <<s { 𝑝 } → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 )
62 60 61 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 )
63 62 r19.21bi ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 )
64 vex ⊢ 𝑝 ∈ V
65 breq2 ⊢ ( 𝑦 = 𝑝 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝 ) )
66 64 65 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑝 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑝 )
67 63 66 sylib ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 <s 𝑝 )
68 simprrl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑝 <s 𝑟 )
69 68 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑝 <s 𝑟 )
70 55 57 58 67 69 slttrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 <s 𝑟 )
71 vex ⊢ 𝑟 ∈ V
72 breq2 ⊢ ( 𝑦 = 𝑟 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟 ) )
73 71 72 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝑟 )
74 70 73 sylibr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 )
75 74 ralrimiva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 )
76 52 54 75 3jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( 𝐴 ⊆ No ∧ { 𝑟 } ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 ) )
77 brsslt ⊢ ( 𝐴 <<s { 𝑟 } ↔ ( ( 𝐴 ∈ V ∧ { 𝑟 } ∈ V ) ∧ ( 𝐴 ⊆ No ∧ { 𝑟 } ⊆ No ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ { 𝑟 } 𝑥 <s 𝑦 ) ) )
78 51 76 77 sylanbrc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐴 <<s { 𝑟 } )
79 4 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐵 ∈ V )
80 79 50 jctil ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( { 𝑟 } ∈ V ∧ 𝐵 ∈ V ) )
81 3 ad2antrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝐵 ⊆ No )
82 48 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 ∈ No )
83 simplr2 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑞 ∈ No )
84 83 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑞 ∈ No )
85 81 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ No )
86 simprrr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → 𝑟 <s 𝑞 )
87 86 adantr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 <s 𝑞 )
88 simplrr ⊢ ( ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) → { 𝑞 } <<s 𝐵 )
89 88 adantl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → { 𝑞 } <<s 𝐵 )
90 ssltsep ⊢ ( { 𝑞 } <<s 𝐵 → ∀ 𝑥 ∈ { 𝑞 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
91 89 90 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ { 𝑞 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
92 vex ⊢ 𝑞 ∈ V
93 breq1 ⊢ ( 𝑥 = 𝑞 → ( 𝑥 <s 𝑦 ↔ 𝑞 <s 𝑦 ) )
94 93 ralbidv ⊢ ( 𝑥 = 𝑞 → ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑞 <s 𝑦 ) )
95 92 94 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝑞 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑞 <s 𝑦 )
96 91 95 sylib ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑦 ∈ 𝐵 𝑞 <s 𝑦 )
97 96 r19.21bi ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑞 <s 𝑦 )
98 82 84 85 87 97 slttrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑟 <s 𝑦 )
99 98 ralrimiva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑦 ∈ 𝐵 𝑟 <s 𝑦 )
100 breq1 ⊢ ( 𝑥 = 𝑟 → ( 𝑥 <s 𝑦 ↔ 𝑟 <s 𝑦 ) )
101 100 ralbidv ⊢ ( 𝑥 = 𝑟 → ( ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑟 <s 𝑦 ) )
102 71 101 ralsn ⊢ ( ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 𝑟 <s 𝑦 )
103 99 102 sylibr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 )
104 54 81 103 3jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( { 𝑟 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) )
105 brsslt ⊢ ( { 𝑟 } <<s 𝐵 ↔ ( ( { 𝑟 } ∈ V ∧ 𝐵 ∈ V ) ∧ ( { 𝑟 } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑥 ∈ { 𝑟 } ∀ 𝑦 ∈ 𝐵 𝑥 <s 𝑦 ) ) )
106 80 104 105 sylanbrc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → { 𝑟 } <<s 𝐵 )
107 48 78 106 jca32 ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) ∧ ( ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ∧ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) ∧ ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) ) ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) )
108 107 exp44 ⊢ ( ( 𝐴 <<s 𝐵 ∧ ( 𝑝 ∈ No ∧ 𝑞 ∈ No ∧ 𝑟 ∈ No ) ) → ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
109 108 ralrimivvva ⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑝 ∈ No ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
110 sneq ⊢ ( 𝑦 = 𝑝 → { 𝑦 } = { 𝑝 } )
111 110 breq2d ⊢ ( 𝑦 = 𝑝 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑝 } ) )
112 110 breq1d ⊢ ( 𝑦 = 𝑝 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑝 } <<s 𝐵 ) )
113 111 112 anbi12d ⊢ ( 𝑦 = 𝑝 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) ) )
114 113 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 𝐵 ) ) ) ) ) )
115 sneq ⊢ ( 𝑦 = 𝑞 → { 𝑦 } = { 𝑞 } )
116 115 breq2d ⊢ ( 𝑦 = 𝑞 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑞 } ) )
117 115 breq1d ⊢ ( 𝑦 = 𝑞 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑞 } <<s 𝐵 ) )
118 116 117 anbi12d ⊢ ( 𝑦 = 𝑞 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) ) )
119 118 ralrab ⊢ ( ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ↔ ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
120 sneq ⊢ ( 𝑦 = 𝑟 → { 𝑦 } = { 𝑟 } )
121 120 breq2d ⊢ ( 𝑦 = 𝑟 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑟 } ) )
122 120 breq1d ⊢ ( 𝑦 = 𝑟 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑟 } <<s 𝐵 ) )
123 121 122 anbi12d ⊢ ( 𝑦 = 𝑟 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) )
124 123 elrab ⊢ ( 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) )
125 124 imbi2i ⊢ ( ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) )
126 125 ralbii ⊢ ( ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) )
127 126 ralbii ⊢ ( ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) )
128 r19.21v ⊢ ( ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
129 128 ralbii ⊢ ( ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ↔ ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
130 119 127 129 3bitr4i ⊢ ( ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ↔ ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) )
131 130 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 𝐵 ) ) ) ) )
132 r19.21v ⊢ ( ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
133 132 ralbii ⊢ ( ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
134 r19.21v ⊢ ( ∀ 𝑞 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
135 133 134 bitri ⊢ ( ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) ↔ ( ( 𝐴 <<s { 𝑝 } ∧ { 𝑝 } <<s 𝐵 ) → ∀ 𝑞 ∈ No ∀ 𝑟 ∈ No ( ( 𝐴 <<s { 𝑞 } ∧ { 𝑞 } <<s 𝐵 ) → ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → ( 𝑟 ∈ No ∧ ( 𝐴 <<s { 𝑟 } ∧ { 𝑟 } <<s 𝐵 ) ) ) ) ) )
136 135 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 𝐵 ) ) ) ) ) )
137 114 131 136 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 𝐵 ) ) ) ) ) )
138 109 137 sylibr ⊢ ( 𝐴 <<s 𝐵 → ∀ 𝑝 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑞 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ∀ 𝑟 ∈ No ( ( 𝑝 <s 𝑟 ∧ 𝑟 <s 𝑞 ) → 𝑟 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
139 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 𝐵 ) } ) )
140 45 47 138 139 syl3anc ⊢ ( 𝐴 <<s 𝐵 → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )