Metamath Proof Explorer

Theorem lesrec

Description: A comparison law for surreals considered as cuts of sets of surreals. Definition from Conway p. 4. Theorem 4 of Alling p. 186. Theorem 2.5 of Gonshor p. 9. (Contributed by Scott Fenton, 11-Dec-2021)

Ref Expression
Assertion lesrec ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 cutscl ⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ No )
2 1 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐴 |s 𝐵 ) ∈ No )
3 cutscl ⊢ ( 𝐶 <<s 𝐷 → ( 𝐶 |s 𝐷 ) ∈ No )
4 3 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐶 |s 𝐷 ) ∈ No )
5 sltsss2 ⊢ ( 𝐶 <<s 𝐷 → 𝐷 ⊆ No )
6 5 ad2antlr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → 𝐷 ⊆ No )
7 6 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ No )
8 simplr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) )
9 cutcuts ⊢ ( 𝐶 <<s 𝐷 → ( ( 𝐶 |s 𝐷 ) ∈ No ∧ 𝐶 <<s { ( 𝐶 |s 𝐷 ) } ∧ { ( 𝐶 |s 𝐷 ) } <<s 𝐷 ) )
10 9 simp3d ⊢ ( 𝐶 <<s 𝐷 → { ( 𝐶 |s 𝐷 ) } <<s 𝐷 )
11 10 ad2antlr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → { ( 𝐶 |s 𝐷 ) } <<s 𝐷 )
12 sltssep ⊢ ( { ( 𝐶 |s 𝐷 ) } <<s 𝐷 → ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 )
13 11 12 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 )
14 ovex ⊢ ( 𝐶 |s 𝐷 ) ∈ V
15 breq1 ⊢ ( 𝑎 = ( 𝐶 |s 𝐷 ) → ( 𝑎 <s 𝑑 ↔ ( 𝐶 |s 𝐷 ) <s 𝑑 ) )
16 15 ralbidv ⊢ ( 𝑎 = ( 𝐶 |s 𝐷 ) → ( ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀ 𝑑 ∈ 𝐷 ( 𝐶 |s 𝐷 ) <s 𝑑 ) )
17 14 16 ralsn ⊢ ( ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀ 𝑑 ∈ 𝐷 ( 𝐶 |s 𝐷 ) <s 𝑑 )
18 13 17 sylib ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → ∀ 𝑑 ∈ 𝐷 ( 𝐶 |s 𝐷 ) <s 𝑑 )
19 18 r19.21bi ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐶 |s 𝐷 ) <s 𝑑 )
20 2 4 7 8 19 leltstrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( 𝐴 |s 𝐵 ) <s 𝑑 )
21 20 ralrimiva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 )
22 sltsss1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ⊆ No )
23 22 adantr ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) → 𝐴 ⊆ No )
24 23 adantr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → 𝐴 ⊆ No )
25 24 sselda ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ No )
26 1 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐴 |s 𝐵 ) ∈ No )
27 3 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐶 |s 𝐷 ) ∈ No )
28 cutcuts ⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
29 28 simp2d ⊢ ( 𝐴 <<s 𝐵 → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
30 29 adantr ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
31 30 adantr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → 𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
32 sltssep ⊢ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } → ∀ 𝑎 ∈ 𝐴 ∀ 𝑑 ∈ { ( 𝐴 |s 𝐵 ) } 𝑎 <s 𝑑 )
33 31 32 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑑 ∈ { ( 𝐴 |s 𝐵 ) } 𝑎 <s 𝑑 )
34 33 r19.21bi ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑑 ∈ { ( 𝐴 |s 𝐵 ) } 𝑎 <s 𝑑 )
35 ovex ⊢ ( 𝐴 |s 𝐵 ) ∈ V
36 breq2 ⊢ ( 𝑑 = ( 𝐴 |s 𝐵 ) → ( 𝑎 <s 𝑑 ↔ 𝑎 <s ( 𝐴 |s 𝐵 ) ) )
37 35 36 ralsn ⊢ ( ∀ 𝑑 ∈ { ( 𝐴 |s 𝐵 ) } 𝑎 <s 𝑑 ↔ 𝑎 <s ( 𝐴 |s 𝐵 ) )
38 34 37 sylib ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s ( 𝐴 |s 𝐵 ) )
39 simplr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) )
40 25 26 27 38 39 ltlestrd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 <s ( 𝐶 |s 𝐷 ) )
41 40 ralrimiva ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) )
42 21 41 jca ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) → ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) )
43 bdayon ⊢ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On
44 43 onordi ⊢ Ord ( bday ‘ ( 𝐴 |s 𝐵 ) )
45 ordn2lp ⊢ ( Ord ( bday ‘ ( 𝐴 |s 𝐵 ) ) → ¬ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∧ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) )
46 44 45 ax-mp ⊢ ¬ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∧ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
47 3 ad2antlr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( 𝐶 |s 𝐷 ) ∈ No )
48 1 adantr ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) → ( 𝐴 |s 𝐵 ) ∈ No )
49 48 adantr ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( 𝐴 |s 𝐵 ) ∈ No )
50 ltnles ⊢ ( ( ( 𝐶 |s 𝐷 ) ∈ No ∧ ( 𝐴 |s 𝐵 ) ∈ No ) → ( ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ↔ ¬ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) )
51 47 49 50 syl2anc ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ↔ ¬ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) )
52 3 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐶 |s 𝐷 ) ∈ No )
53 sltsex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
54 53 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐴 ∈ V )
55 snex ⊢ { ( 𝐶 |s 𝐷 ) } ∈ V
56 54 55 jctir ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐴 ∈ V ∧ { ( 𝐶 |s 𝐷 ) } ∈ V ) )
57 22 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐴 ⊆ No )
58 52 snssd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → { ( 𝐶 |s 𝐷 ) } ⊆ No )
59 simplrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) )
60 breq2 ⊢ ( 𝑑 = ( 𝐶 |s 𝐷 ) → ( 𝑎 <s 𝑑 ↔ 𝑎 <s ( 𝐶 |s 𝐷 ) ) )
61 14 60 ralsn ⊢ ( ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑎 <s 𝑑 ↔ 𝑎 <s ( 𝐶 |s 𝐷 ) )
62 61 ralbii ⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑎 <s 𝑑 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) )
63 59 62 sylibr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑎 <s 𝑑 )
64 57 58 63 3jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐴 ⊆ No ∧ { ( 𝐶 |s 𝐷 ) } ⊆ No ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑎 <s 𝑑 ) )
65 brslts ⊢ ( 𝐴 <<s { ( 𝐶 |s 𝐷 ) } ↔ ( ( 𝐴 ∈ V ∧ { ( 𝐶 |s 𝐷 ) } ∈ V ) ∧ ( 𝐴 ⊆ No ∧ { ( 𝐶 |s 𝐷 ) } ⊆ No ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑎 <s 𝑑 ) ) )
66 56 64 65 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐴 <<s { ( 𝐶 |s 𝐷 ) } )
67 sltsex2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ∈ V )
68 67 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐵 ∈ V )
69 68 55 jctil ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( { ( 𝐶 |s 𝐷 ) } ∈ V ∧ 𝐵 ∈ V ) )
70 sltsss2 ⊢ ( 𝐴 <<s 𝐵 → 𝐵 ⊆ No )
71 70 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐵 ⊆ No )
72 52 adantr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐶 |s 𝐷 ) ∈ No )
73 48 ad3antrrr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) ∈ No )
74 71 sselda ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ No )
75 simplr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) )
76 28 simp3d ⊢ ( 𝐴 <<s 𝐵 → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
77 76 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
78 sltssep ⊢ ( { ( 𝐴 |s 𝐵 ) } <<s 𝐵 → ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 )
79 77 78 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 )
80 breq1 ⊢ ( 𝑎 = ( 𝐴 |s 𝐵 ) → ( 𝑎 <s 𝑏 ↔ ( 𝐴 |s 𝐵 ) <s 𝑏 ) )
81 80 ralbidv ⊢ ( 𝑎 = ( 𝐴 |s 𝐵 ) → ( ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 ( 𝐴 |s 𝐵 ) <s 𝑏 ) )
82 35 81 ralsn ⊢ ( ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 ( 𝐴 |s 𝐵 ) <s 𝑏 )
83 79 82 sylib ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑏 ∈ 𝐵 ( 𝐴 |s 𝐵 ) <s 𝑏 )
84 83 r19.21bi ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐴 |s 𝐵 ) <s 𝑏 )
85 72 73 74 75 84 ltstrd ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑏 ∈ 𝐵 ) → ( 𝐶 |s 𝐷 ) <s 𝑏 )
86 85 ralrimiva ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑏 ∈ 𝐵 ( 𝐶 |s 𝐷 ) <s 𝑏 )
87 breq1 ⊢ ( 𝑎 = ( 𝐶 |s 𝐷 ) → ( 𝑎 <s 𝑏 ↔ ( 𝐶 |s 𝐷 ) <s 𝑏 ) )
88 87 ralbidv ⊢ ( 𝑎 = ( 𝐶 |s 𝐷 ) → ( ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 ( 𝐶 |s 𝐷 ) <s 𝑏 ) )
89 14 88 ralsn ⊢ ( ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ↔ ∀ 𝑏 ∈ 𝐵 ( 𝐶 |s 𝐷 ) <s 𝑏 )
90 86 89 sylibr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 )
91 58 71 90 3jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( { ( 𝐶 |s 𝐷 ) } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) )
92 brslts ⊢ ( { ( 𝐶 |s 𝐷 ) } <<s 𝐵 ↔ ( ( { ( 𝐶 |s 𝐷 ) } ∈ V ∧ 𝐵 ∈ V ) ∧ ( { ( 𝐶 |s 𝐷 ) } ⊆ No ∧ 𝐵 ⊆ No ∧ ∀ 𝑎 ∈ { ( 𝐶 |s 𝐷 ) } ∀ 𝑏 ∈ 𝐵 𝑎 <s 𝑏 ) ) )
93 69 91 92 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → { ( 𝐶 |s 𝐷 ) } <<s 𝐵 )
94 ltsirr ⊢ ( ( 𝐴 |s 𝐵 ) ∈ No → ¬ ( 𝐴 |s 𝐵 ) <s ( 𝐴 |s 𝐵 ) )
95 49 94 syl ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ¬ ( 𝐴 |s 𝐵 ) <s ( 𝐴 |s 𝐵 ) )
96 breq1 ⊢ ( ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) → ( ( 𝐴 |s 𝐵 ) <s ( 𝐴 |s 𝐵 ) ↔ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) )
97 96 notbid ⊢ ( ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) → ( ¬ ( 𝐴 |s 𝐵 ) <s ( 𝐴 |s 𝐵 ) ↔ ¬ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) )
98 95 97 syl5ibcom ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( ( 𝐴 |s 𝐵 ) = ( 𝐶 |s 𝐷 ) → ¬ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) )
99 98 necon2ad ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) → ( 𝐴 |s 𝐵 ) ≠ ( 𝐶 |s 𝐷 ) ) )
100 99 imp ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐴 |s 𝐵 ) ≠ ( 𝐶 |s 𝐷 ) )
101 100 necomd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐶 |s 𝐷 ) ≠ ( 𝐴 |s 𝐵 ) )
102 cutbdaylt ⊢ ( ( ( 𝐶 |s 𝐷 ) ∈ No ∧ ( 𝐴 <<s { ( 𝐶 |s 𝐷 ) } ∧ { ( 𝐶 |s 𝐷 ) } <<s 𝐵 ) ∧ ( 𝐶 |s 𝐷 ) ≠ ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) )
103 52 66 93 101 102 syl121anc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) )
104 1 ad3antrrr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐴 |s 𝐵 ) ∈ No )
105 sltsex1 ⊢ ( 𝐶 <<s 𝐷 → 𝐶 ∈ V )
106 105 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐶 ∈ V )
107 snex ⊢ { ( 𝐴 |s 𝐵 ) } ∈ V
108 106 107 jctir ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐶 ∈ V ∧ { ( 𝐴 |s 𝐵 ) } ∈ V ) )
109 sltsss1 ⊢ ( 𝐶 <<s 𝐷 → 𝐶 ⊆ No )
110 109 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐶 ⊆ No )
111 104 snssd ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → { ( 𝐴 |s 𝐵 ) } ⊆ No )
112 110 sselda ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 ∈ No )
113 52 adantr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝐶 |s 𝐷 ) ∈ No )
114 48 ad3antrrr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝐴 |s 𝐵 ) ∈ No )
115 9 simp2d ⊢ ( 𝐶 <<s 𝐷 → 𝐶 <<s { ( 𝐶 |s 𝐷 ) } )
116 115 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐶 <<s { ( 𝐶 |s 𝐷 ) } )
117 sltssep ⊢ ( 𝐶 <<s { ( 𝐶 |s 𝐷 ) } → ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑐 <s 𝑑 )
118 116 117 syl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑐 ∈ 𝐶 ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑐 <s 𝑑 )
119 118 r19.21bi ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑐 <s 𝑑 )
120 breq2 ⊢ ( 𝑑 = ( 𝐶 |s 𝐷 ) → ( 𝑐 <s 𝑑 ↔ 𝑐 <s ( 𝐶 |s 𝐷 ) ) )
121 14 120 ralsn ⊢ ( ∀ 𝑑 ∈ { ( 𝐶 |s 𝐷 ) } 𝑐 <s 𝑑 ↔ 𝑐 <s ( 𝐶 |s 𝐷 ) )
122 119 121 sylib ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 <s ( 𝐶 |s 𝐷 ) )
123 simplr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) )
124 112 113 114 122 123 ltstrd ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → 𝑐 <s ( 𝐴 |s 𝐵 ) )
125 breq2 ⊢ ( 𝑎 = ( 𝐴 |s 𝐵 ) → ( 𝑐 <s 𝑎 ↔ 𝑐 <s ( 𝐴 |s 𝐵 ) ) )
126 35 125 ralsn ⊢ ( ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } 𝑐 <s 𝑎 ↔ 𝑐 <s ( 𝐴 |s 𝐵 ) )
127 124 126 sylibr ⊢ ( ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) ∧ 𝑐 ∈ 𝐶 ) → ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } 𝑐 <s 𝑎 )
128 127 ralrimiva ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑐 ∈ 𝐶 ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } 𝑐 <s 𝑎 )
129 110 111 128 3jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( 𝐶 ⊆ No ∧ { ( 𝐴 |s 𝐵 ) } ⊆ No ∧ ∀ 𝑐 ∈ 𝐶 ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } 𝑐 <s 𝑎 ) )
130 brslts ⊢ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ↔ ( ( 𝐶 ∈ V ∧ { ( 𝐴 |s 𝐵 ) } ∈ V ) ∧ ( 𝐶 ⊆ No ∧ { ( 𝐴 |s 𝐵 ) } ⊆ No ∧ ∀ 𝑐 ∈ 𝐶 ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } 𝑐 <s 𝑎 ) ) )
131 108 129 130 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐶 <<s { ( 𝐴 |s 𝐵 ) } )
132 sltsex2 ⊢ ( 𝐶 <<s 𝐷 → 𝐷 ∈ V )
133 132 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐷 ∈ V )
134 133 107 jctil ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( { ( 𝐴 |s 𝐵 ) } ∈ V ∧ 𝐷 ∈ V ) )
135 5 ad3antlr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → 𝐷 ⊆ No )
136 simplrl ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 )
137 breq1 ⊢ ( 𝑎 = ( 𝐴 |s 𝐵 ) → ( 𝑎 <s 𝑑 ↔ ( 𝐴 |s 𝐵 ) <s 𝑑 ) )
138 137 ralbidv ⊢ ( 𝑎 = ( 𝐴 |s 𝐵 ) → ( ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ) )
139 35 138 ralsn ⊢ ( ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 )
140 136 139 sylibr ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 )
141 111 135 140 3jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( { ( 𝐴 |s 𝐵 ) } ⊆ No ∧ 𝐷 ⊆ No ∧ ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 ) )
142 brslts ⊢ ( { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ↔ ( ( { ( 𝐴 |s 𝐵 ) } ∈ V ∧ 𝐷 ∈ V ) ∧ ( { ( 𝐴 |s 𝐵 ) } ⊆ No ∧ 𝐷 ⊆ No ∧ ∀ 𝑎 ∈ { ( 𝐴 |s 𝐵 ) } ∀ 𝑑 ∈ 𝐷 𝑎 <s 𝑑 ) ) )
143 134 141 142 sylanbrc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → { ( 𝐴 |s 𝐵 ) } <<s 𝐷 )
144 cutbdaylt ⊢ ( ( ( 𝐴 |s 𝐵 ) ∈ No ∧ ( 𝐶 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐷 ) ∧ ( 𝐴 |s 𝐵 ) ≠ ( 𝐶 |s 𝐷 ) ) → ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
145 104 131 143 100 144 syl121anc ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) )
146 103 145 jca ⊢ ( ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ∧ ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∧ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) )
147 146 ex ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( ( 𝐶 |s 𝐷 ) <s ( 𝐴 |s 𝐵 ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∧ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) ) )
148 51 147 sylbird ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( ¬ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∧ ( bday ‘ ( 𝐶 |s 𝐷 ) ) ∈ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) ) )
149 46 148 mt3i ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) → ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) )
150 42 149 impbida ⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) → ( ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ↔ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) )
151 breq12 ⊢ ( ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) → ( 𝑋 ≤s 𝑌 ↔ ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ) )
152 breq1 ⊢ ( 𝑋 = ( 𝐴 |s 𝐵 ) → ( 𝑋 <s 𝑑 ↔ ( 𝐴 |s 𝐵 ) <s 𝑑 ) )
153 152 ralbidv ⊢ ( 𝑋 = ( 𝐴 |s 𝐵 ) → ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ↔ ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ) )
154 breq2 ⊢ ( 𝑌 = ( 𝐶 |s 𝐷 ) → ( 𝑎 <s 𝑌 ↔ 𝑎 <s ( 𝐶 |s 𝐷 ) ) )
155 154 ralbidv ⊢ ( 𝑌 = ( 𝐶 |s 𝐷 ) → ( ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ↔ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) )
156 153 155 bi2anan9 ⊢ ( ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) → ( ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ↔ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) )
157 151 156 bibi12d ⊢ ( ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) → ( ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) ↔ ( ( 𝐴 |s 𝐵 ) ≤s ( 𝐶 |s 𝐷 ) ↔ ( ∀ 𝑑 ∈ 𝐷 ( 𝐴 |s 𝐵 ) <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s ( 𝐶 |s 𝐷 ) ) ) ) )
158 150 157 imbitrrid ⊢ ( ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) → ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) → ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) ) )
159 158 impcom ⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝐶 <<s 𝐷 ) ∧ ( 𝑋 = ( 𝐴 |s 𝐵 ) ∧ 𝑌 = ( 𝐶 |s 𝐷 ) ) ) → ( 𝑋 ≤s 𝑌 ↔ ( ∀ 𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀ 𝑎 ∈ 𝐴 𝑎 <s 𝑌 ) ) )