Metamath Proof Explorer

Theorem eqcuts3

Description: A variant of the simplicity theorem - if B lies between the cut sets of A but none of its options do, then A = B . Theorem 11 of Conway p. 23. (Contributed by Scott Fenton, 28-Nov-2025)

Ref Expression
Hypotheses eqcuts3.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
eqcuts3.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
eqcuts3.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
eqcuts3.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
eqcuts3.5 ⊢ ( 𝜑 → 𝐿 <<s { 𝐵 } )
eqcuts3.6 ⊢ ( 𝜑 → { 𝐵 } <<s 𝑅 )
eqcuts3.7 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( 𝑀 ∪ 𝑆 ) ¬ ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) )
Assertion eqcuts3 ( 𝜑 → 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 eqcuts3.1 ⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2 eqcuts3.2 ⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3 eqcuts3.3 ⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
4 eqcuts3.4 ⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
5 eqcuts3.5 ⊢ ( 𝜑 → 𝐿 <<s { 𝐵 } )
6 eqcuts3.6 ⊢ ( 𝜑 → { 𝐵 } <<s 𝑅 )
7 eqcuts3.7 ⊢ ( 𝜑 → ∀ 𝑥𝑂 ∈ ( 𝑀 ∪ 𝑆 ) ¬ ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) )
8 sneq ⊢ ( 𝑥𝑂 = 𝑧𝑅 → { 𝑥𝑂 } = { 𝑧𝑅 } )
9 8 breq2d ⊢ ( 𝑥𝑂 = 𝑧𝑅 → ( 𝐿 <<s { 𝑥𝑂 } ↔ 𝐿 <<s { 𝑧𝑅 } ) )
10 8 breq1d ⊢ ( 𝑥𝑂 = 𝑧𝑅 → ( { 𝑥𝑂 } <<s 𝑅 ↔ { 𝑧𝑅 } <<s 𝑅 ) )
11 9 10 anbi12d ⊢ ( 𝑥𝑂 = 𝑧𝑅 → ( ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) ↔ ( 𝐿 <<s { 𝑧𝑅 } ∧ { 𝑧𝑅 } <<s 𝑅 ) ) )
12 11 notbid ⊢ ( 𝑥𝑂 = 𝑧𝑅 → ( ¬ ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) ↔ ¬ ( 𝐿 <<s { 𝑧𝑅 } ∧ { 𝑧𝑅 } <<s 𝑅 ) ) )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → ∀ 𝑥𝑂 ∈ ( 𝑀 ∪ 𝑆 ) ¬ ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) )
14 elun2 ⊢ ( 𝑧𝑅 ∈ 𝑆 → 𝑧𝑅 ∈ ( 𝑀 ∪ 𝑆 ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → 𝑧𝑅 ∈ ( 𝑀 ∪ 𝑆 ) )
16 12 13 15 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → ¬ ( 𝐿 <<s { 𝑧𝑅 } ∧ { 𝑧𝑅 } <<s 𝑅 ) )
17 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → 𝐿 <<s { 𝐵 } )
18 4 sneqd ⊢ ( 𝜑 → { 𝐵 } = { ( 𝑀 |s 𝑆 ) } )
19 cutcuts ⊢ ( 𝑀 <<s 𝑆 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
20 2 19 syl ⊢ ( 𝜑 → ( ( 𝑀 |s 𝑆 ) ∈ No ∧ 𝑀 <<s { ( 𝑀 |s 𝑆 ) } ∧ { ( 𝑀 |s 𝑆 ) } <<s 𝑆 ) )
21 20 simp3d ⊢ ( 𝜑 → { ( 𝑀 |s 𝑆 ) } <<s 𝑆 )
22 18 21 eqbrtrd ⊢ ( 𝜑 → { 𝐵 } <<s 𝑆 )
23 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝐵 } <<s 𝑆 )
24 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → 𝑧𝑅 ∈ 𝑆 )
25 24 snssd ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝑧𝑅 } ⊆ 𝑆 )
26 ssslts2 ⊢ ( ( { 𝐵 } <<s 𝑆 ∧ { 𝑧𝑅 } ⊆ 𝑆 ) → { 𝐵 } <<s { 𝑧𝑅 } )
27 23 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝐵 } <<s { 𝑧𝑅 } )
28 2 cutscld ⊢ ( 𝜑 → ( 𝑀 |s 𝑆 ) ∈ No )
29 4 28 eqeltrd ⊢ ( 𝜑 → 𝐵 ∈ No )
30 snnzg ⊢ ( 𝐵 ∈ No → { 𝐵 } ≠ ∅ )
31 29 30 syl ⊢ ( 𝜑 → { 𝐵 } ≠ ∅ )
32 31 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝐵 } ≠ ∅ )
33 sltstr ⊢ ( ( 𝐿 <<s { 𝐵 } ∧ { 𝐵 } <<s { 𝑧𝑅 } ∧ { 𝐵 } ≠ ∅ ) → 𝐿 <<s { 𝑧𝑅 } )
34 17 27 32 33 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → 𝐿 <<s { 𝑧𝑅 } )
35 snex ⊢ { 𝑧𝑅 } ∈ V
36 35 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝑧𝑅 } ∈ V )
37 sltsex2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ∈ V )
38 1 37 syl ⊢ ( 𝜑 → 𝑅 ∈ V )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → 𝑅 ∈ V )
40 sltsss2 ⊢ ( { 𝐵 } <<s { 𝑧𝑅 } → { 𝑧𝑅 } ⊆ No )
41 27 40 syl ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝑧𝑅 } ⊆ No )
42 sltsss2 ⊢ ( 𝐿 <<s 𝑅 → 𝑅 ⊆ No )
43 1 42 syl ⊢ ( 𝜑 → 𝑅 ⊆ No )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → 𝑅 ⊆ No )
45 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) )
46 sltsss2 ⊢ ( 𝑀 <<s 𝑆 → 𝑆 ⊆ No )
47 2 46 syl ⊢ ( 𝜑 → 𝑆 ⊆ No )
48 47 sselda ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → 𝑧𝑅 ∈ No )
49 45 48 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝑧𝑅 ∈ No )
50 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝜑 )
51 1 cutscld ⊢ ( 𝜑 → ( 𝐿 |s 𝑅 ) ∈ No )
52 3 51 eqeltrd ⊢ ( 𝜑 → 𝐴 ∈ No )
53 50 52 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝐴 ∈ No )
54 44 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝑥𝑅 ∈ No )
55 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝑧𝑅 ≤s 𝐴 )
56 cutcuts ⊢ ( 𝐿 <<s 𝑅 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
57 1 56 syl ⊢ ( 𝜑 → ( ( 𝐿 |s 𝑅 ) ∈ No ∧ 𝐿 <<s { ( 𝐿 |s 𝑅 ) } ∧ { ( 𝐿 |s 𝑅 ) } <<s 𝑅 ) )
58 57 simp3d ⊢ ( 𝜑 → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
60 59 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → { ( 𝐿 |s 𝑅 ) } <<s 𝑅 )
61 ovex ⊢ ( 𝐿 |s 𝑅 ) ∈ V
62 61 elsn2 ⊢ ( 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } ↔ 𝐴 = ( 𝐿 |s 𝑅 ) )
63 3 62 sylibr ⊢ ( 𝜑 → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
65 64 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
66 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝑥𝑅 ∈ 𝑅 )
67 60 65 66 sltssepcd ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝐴 <s 𝑥𝑅 )
68 49 53 54 55 67 leltstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝑧𝑅 <s 𝑥𝑅 )
69 velsn ⊢ ( 𝑥 ∈ { 𝑧𝑅 } ↔ 𝑥 = 𝑧𝑅 )
70 breq1 ⊢ ( 𝑥 = 𝑧𝑅 → ( 𝑥 <s 𝑥𝑅 ↔ 𝑧𝑅 <s 𝑥𝑅 ) )
71 69 70 sylbi ⊢ ( 𝑥 ∈ { 𝑧𝑅 } → ( 𝑥 <s 𝑥𝑅 ↔ 𝑧𝑅 <s 𝑥𝑅 ) )
72 68 71 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥𝑅 ∈ 𝑅 ) → ( 𝑥 ∈ { 𝑧𝑅 } → 𝑥 <s 𝑥𝑅 ) )
73 72 ex ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → ( 𝑥𝑅 ∈ 𝑅 → ( 𝑥 ∈ { 𝑧𝑅 } → 𝑥 <s 𝑥𝑅 ) ) )
74 73 com23 ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → ( 𝑥 ∈ { 𝑧𝑅 } → ( 𝑥𝑅 ∈ 𝑅 → 𝑥 <s 𝑥𝑅 ) ) )
75 74 3imp ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) ∧ 𝑥 ∈ { 𝑧𝑅 } ∧ 𝑥𝑅 ∈ 𝑅 ) → 𝑥 <s 𝑥𝑅 )
76 36 39 41 44 75 sltsd ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → { 𝑧𝑅 } <<s 𝑅 )
77 34 76 jca ⊢ ( ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) ∧ 𝑧𝑅 ≤s 𝐴 ) → ( 𝐿 <<s { 𝑧𝑅 } ∧ { 𝑧𝑅 } <<s 𝑅 ) )
78 16 77 mtand ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → ¬ 𝑧𝑅 ≤s 𝐴 )
79 52 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → 𝐴 ∈ No )
80 ltnles ⊢ ( ( 𝐴 ∈ No ∧ 𝑧𝑅 ∈ No ) → ( 𝐴 <s 𝑧𝑅 ↔ ¬ 𝑧𝑅 ≤s 𝐴 ) )
81 79 48 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → ( 𝐴 <s 𝑧𝑅 ↔ ¬ 𝑧𝑅 ≤s 𝐴 ) )
82 78 81 mpbird ⊢ ( ( 𝜑 ∧ 𝑧𝑅 ∈ 𝑆 ) → 𝐴 <s 𝑧𝑅 )
83 82 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧𝑅 ∈ 𝑆 𝐴 <s 𝑧𝑅 )
84 sltssep ⊢ ( 𝐿 <<s { 𝐵 } → ∀ 𝑥 ∈ 𝐿 ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 )
85 5 84 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐿 ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 )
86 breq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐵 ) )
87 86 ralsng ⊢ ( 𝐵 ∈ No → ( ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐵 ) )
88 29 87 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐵 ) )
89 88 ralbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐿 ∀ 𝑦 ∈ { 𝐵 } 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐿 𝑥 <s 𝐵 ) )
90 85 89 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐿 𝑥 <s 𝐵 )
91 1 2 3 4 lesrecd ⊢ ( 𝜑 → ( 𝐴 ≤s 𝐵 ↔ ( ∀ 𝑧𝑅 ∈ 𝑆 𝐴 <s 𝑧𝑅 ∧ ∀ 𝑥 ∈ 𝐿 𝑥 <s 𝐵 ) ) )
92 83 90 91 mpbir2and ⊢ ( 𝜑 → 𝐴 ≤s 𝐵 )
93 sltssep ⊢ ( { 𝐵 } <<s 𝑅 → ∀ 𝑥 ∈ { 𝐵 } ∀ 𝑦 ∈ 𝑅 𝑥 <s 𝑦 )
94 6 93 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝐵 } ∀ 𝑦 ∈ 𝑅 𝑥 <s 𝑦 )
95 breq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 <s 𝑦 ↔ 𝐵 <s 𝑦 ) )
96 95 ralbidv ⊢ ( 𝑥 = 𝐵 → ( ∀ 𝑦 ∈ 𝑅 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝑅 𝐵 <s 𝑦 ) )
97 96 ralsng ⊢ ( 𝐵 ∈ No → ( ∀ 𝑥 ∈ { 𝐵 } ∀ 𝑦 ∈ 𝑅 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝑅 𝐵 <s 𝑦 ) )
98 29 97 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐵 } ∀ 𝑦 ∈ 𝑅 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ 𝑅 𝐵 <s 𝑦 ) )
99 94 98 mpbid ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑅 𝐵 <s 𝑦 )
100 sneq ⊢ ( 𝑥𝑂 = 𝑧𝐿 → { 𝑥𝑂 } = { 𝑧𝐿 } )
101 100 breq2d ⊢ ( 𝑥𝑂 = 𝑧𝐿 → ( 𝐿 <<s { 𝑥𝑂 } ↔ 𝐿 <<s { 𝑧𝐿 } ) )
102 100 breq1d ⊢ ( 𝑥𝑂 = 𝑧𝐿 → ( { 𝑥𝑂 } <<s 𝑅 ↔ { 𝑧𝐿 } <<s 𝑅 ) )
103 101 102 anbi12d ⊢ ( 𝑥𝑂 = 𝑧𝐿 → ( ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) ↔ ( 𝐿 <<s { 𝑧𝐿 } ∧ { 𝑧𝐿 } <<s 𝑅 ) ) )
104 103 notbid ⊢ ( 𝑥𝑂 = 𝑧𝐿 → ( ¬ ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) ↔ ¬ ( 𝐿 <<s { 𝑧𝐿 } ∧ { 𝑧𝐿 } <<s 𝑅 ) ) )
105 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → ∀ 𝑥𝑂 ∈ ( 𝑀 ∪ 𝑆 ) ¬ ( 𝐿 <<s { 𝑥𝑂 } ∧ { 𝑥𝑂 } <<s 𝑅 ) )
106 elun1 ⊢ ( 𝑧𝐿 ∈ 𝑀 → 𝑧𝐿 ∈ ( 𝑀 ∪ 𝑆 ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝑧𝐿 ∈ ( 𝑀 ∪ 𝑆 ) )
108 104 105 107 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → ¬ ( 𝐿 <<s { 𝑧𝐿 } ∧ { 𝑧𝐿 } <<s 𝑅 ) )
109 sltsex1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ∈ V )
110 1 109 syl ⊢ ( 𝜑 → 𝐿 ∈ V )
111 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝐿 ∈ V )
112 snex ⊢ { 𝑧𝐿 } ∈ V
113 112 a1i ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝑧𝐿 } ∈ V )
114 sltsss1 ⊢ ( 𝐿 <<s 𝑅 → 𝐿 ⊆ No )
115 1 114 syl ⊢ ( 𝜑 → 𝐿 ⊆ No )
116 115 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝐿 ⊆ No )
117 116 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝐿 ⊆ No )
118 simplr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝑧𝐿 ∈ 𝑀 )
119 118 snssd ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝑧𝐿 } ⊆ 𝑀 )
120 sltsss1 ⊢ ( 𝑀 <<s 𝑆 → 𝑀 ⊆ No )
121 2 120 syl ⊢ ( 𝜑 → 𝑀 ⊆ No )
122 121 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝑀 ⊆ No )
123 119 122 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝑧𝐿 } ⊆ No )
124 117 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝑥𝐿 ∈ No )
125 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝜑 )
126 125 52 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝐴 ∈ No )
127 121 sselda ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝑧𝐿 ∈ No )
128 127 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝑧𝐿 ∈ No )
129 128 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝑧𝐿 ∈ No )
130 57 simp2d ⊢ ( 𝜑 → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
132 131 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
133 132 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝐿 <<s { ( 𝐿 |s 𝑅 ) } )
134 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝑥𝐿 ∈ 𝐿 )
135 63 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
136 135 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
137 136 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝐴 ∈ { ( 𝐿 |s 𝑅 ) } )
138 133 134 137 sltssepcd ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝑥𝐿 <s 𝐴 )
139 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝐴 ≤s 𝑧𝐿 )
140 124 126 129 138 139 ltlestrd ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → 𝑥𝐿 <s 𝑧𝐿 )
141 velsn ⊢ ( 𝑥 ∈ { 𝑧𝐿 } ↔ 𝑥 = 𝑧𝐿 )
142 breq2 ⊢ ( 𝑥 = 𝑧𝐿 → ( 𝑥𝐿 <s 𝑥 ↔ 𝑥𝐿 <s 𝑧𝐿 ) )
143 141 142 sylbi ⊢ ( 𝑥 ∈ { 𝑧𝐿 } → ( 𝑥𝐿 <s 𝑥 ↔ 𝑥𝐿 <s 𝑧𝐿 ) )
144 140 143 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ) → ( 𝑥 ∈ { 𝑧𝐿 } → 𝑥𝐿 <s 𝑥 ) )
145 144 3impia ⊢ ( ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) ∧ 𝑥𝐿 ∈ 𝐿 ∧ 𝑥 ∈ { 𝑧𝐿 } ) → 𝑥𝐿 <s 𝑥 )
146 111 113 117 123 145 sltsd ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝐿 <<s { 𝑧𝐿 } )
147 20 simp2d ⊢ ( 𝜑 → 𝑀 <<s { ( 𝑀 |s 𝑆 ) } )
148 147 18 breqtrrd ⊢ ( 𝜑 → 𝑀 <<s { 𝐵 } )
149 148 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝑀 <<s { 𝐵 } )
150 149 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝑀 <<s { 𝐵 } )
151 ssslts1 ⊢ ( ( 𝑀 <<s { 𝐵 } ∧ { 𝑧𝐿 } ⊆ 𝑀 ) → { 𝑧𝐿 } <<s { 𝐵 } )
152 150 119 151 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝑧𝐿 } <<s { 𝐵 } )
153 simpll ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → 𝜑 )
154 153 6 syl ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝐵 } <<s 𝑅 )
155 31 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → { 𝐵 } ≠ ∅ )
156 155 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝐵 } ≠ ∅ )
157 sltstr ⊢ ( ( { 𝑧𝐿 } <<s { 𝐵 } ∧ { 𝐵 } <<s 𝑅 ∧ { 𝐵 } ≠ ∅ ) → { 𝑧𝐿 } <<s 𝑅 )
158 152 154 156 157 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → { 𝑧𝐿 } <<s 𝑅 )
159 146 158 jca ⊢ ( ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) ∧ 𝐴 ≤s 𝑧𝐿 ) → ( 𝐿 <<s { 𝑧𝐿 } ∧ { 𝑧𝐿 } <<s 𝑅 ) )
160 108 159 mtand ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → ¬ 𝐴 ≤s 𝑧𝐿 )
161 52 adantr ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝐴 ∈ No )
162 ltnles ⊢ ( ( 𝑧𝐿 ∈ No ∧ 𝐴 ∈ No ) → ( 𝑧𝐿 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝑧𝐿 ) )
163 127 161 162 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → ( 𝑧𝐿 <s 𝐴 ↔ ¬ 𝐴 ≤s 𝑧𝐿 ) )
164 160 163 mpbird ⊢ ( ( 𝜑 ∧ 𝑧𝐿 ∈ 𝑀 ) → 𝑧𝐿 <s 𝐴 )
165 164 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧𝐿 ∈ 𝑀 𝑧𝐿 <s 𝐴 )
166 2 1 4 3 lesrecd ⊢ ( 𝜑 → ( 𝐵 ≤s 𝐴 ↔ ( ∀ 𝑦 ∈ 𝑅 𝐵 <s 𝑦 ∧ ∀ 𝑧𝐿 ∈ 𝑀 𝑧𝐿 <s 𝐴 ) ) )
167 99 165 166 mpbir2and ⊢ ( 𝜑 → 𝐵 ≤s 𝐴 )
168 lestri3 ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ) )
169 52 29 168 syl2anc ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤s 𝐵 ∧ 𝐵 ≤s 𝐴 ) ) )
170 92 167 169 mpbir2and ⊢ ( 𝜑 → 𝐴 = 𝐵 )