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 φ A s B
cutmax.2 φ X A
cutmax.3 φ y A y s X
Assertion cutmax φ A | s B = X | s B

Proof

Step Hyp Ref Expression
1 cutmax.1 φ A s B
2 cutmax.2 φ X A
3 cutmax.3 φ y A y s X
4 breq2 x = X y s x y s X
5 4 rexsng X A x X y s x y s X
6 2 5 syl φ x X y s x y s X
7 6 ralbidv φ y A x X y s x y A y s X
8 3 7 mpbird φ y A x X y s x
9 simpr φ x B x B
10 ssltss2 A s B B No
11 1 10 syl φ B No
12 11 sselda φ x B x No
13 slerflex x No x s x
14 12 13 syl φ x B x s x
15 breq1 y = x y s x x s x
16 15 rspcev x B x s x y B y s x
17 9 14 16 syl2anc φ x B y B y s x
18 17 ralrimiva φ x B y B y s x
19 scutcut A s B A | s B No A s A | s B A | s B s B
20 1 19 syl φ A | s B No A s A | s B A | s B s B
21 20 simp2d φ A s A | s B
22 2 snssd φ X A
23 sssslt1 A s A | s B X A X s A | s B
24 21 22 23 syl2anc φ X s A | s B
25 20 simp3d φ A | s B s B
26 1 8 18 24 25 cofcut1d φ A | s B = X | s B