Metamath Proof Explorer


Theorem cutmax

Description: If A has a maximum, then the maximum may be used alone in the cut. (Contributed by Scott Fenton, 20-Aug-2025)

Ref Expression
Hypotheses cutmax.1 ( 𝜑𝐴 <<s 𝐵 )
cutmax.2 ( 𝜑𝑋𝐴 )
cutmax.3 ( 𝜑 → ∀ 𝑦𝐴 𝑦 ≤s 𝑋 )
Assertion cutmax ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( { 𝑋 } |s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cutmax.1 ( 𝜑𝐴 <<s 𝐵 )
2 cutmax.2 ( 𝜑𝑋𝐴 )
3 cutmax.3 ( 𝜑 → ∀ 𝑦𝐴 𝑦 ≤s 𝑋 )
4 breq2 ( 𝑥 = 𝑋 → ( 𝑦 ≤s 𝑥𝑦 ≤s 𝑋 ) )
5 4 rexsng ( 𝑋𝐴 → ( ∃ 𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥𝑦 ≤s 𝑋 ) )
6 2 5 syl ( 𝜑 → ( ∃ 𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥𝑦 ≤s 𝑋 ) )
7 6 ralbidv ( 𝜑 → ( ∀ 𝑦𝐴𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥 ↔ ∀ 𝑦𝐴 𝑦 ≤s 𝑋 ) )
8 3 7 mpbird ( 𝜑 → ∀ 𝑦𝐴𝑥 ∈ { 𝑋 } 𝑦 ≤s 𝑥 )
9 simpr ( ( 𝜑𝑥𝐵 ) → 𝑥𝐵 )
10 ssltss2 ( 𝐴 <<s 𝐵𝐵 No )
11 1 10 syl ( 𝜑𝐵 No )
12 11 sselda ( ( 𝜑𝑥𝐵 ) → 𝑥 No )
13 slerflex ( 𝑥 No 𝑥 ≤s 𝑥 )
14 12 13 syl ( ( 𝜑𝑥𝐵 ) → 𝑥 ≤s 𝑥 )
15 breq1 ( 𝑦 = 𝑥 → ( 𝑦 ≤s 𝑥𝑥 ≤s 𝑥 ) )
16 15 rspcev ( ( 𝑥𝐵𝑥 ≤s 𝑥 ) → ∃ 𝑦𝐵 𝑦 ≤s 𝑥 )
17 9 14 16 syl2anc ( ( 𝜑𝑥𝐵 ) → ∃ 𝑦𝐵 𝑦 ≤s 𝑥 )
18 17 ralrimiva ( 𝜑 → ∀ 𝑥𝐵𝑦𝐵 𝑦 ≤s 𝑥 )
19 scutcut ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
20 1 19 syl ( 𝜑 → ( ( 𝐴 |s 𝐵 ) ∈ No 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
21 20 simp2d ( 𝜑𝐴 <<s { ( 𝐴 |s 𝐵 ) } )
22 2 snssd ( 𝜑 → { 𝑋 } ⊆ 𝐴 )
23 sssslt1 ( ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { 𝑋 } ⊆ 𝐴 ) → { 𝑋 } <<s { ( 𝐴 |s 𝐵 ) } )
24 21 22 23 syl2anc ( 𝜑 → { 𝑋 } <<s { ( 𝐴 |s 𝐵 ) } )
25 20 simp3d ( 𝜑 → { ( 𝐴 |s 𝐵 ) } <<s 𝐵 )
26 1 8 18 24 25 cofcut1d ( 𝜑 → ( 𝐴 |s 𝐵 ) = ( { 𝑋 } |s 𝐵 ) )