Metamath Proof Explorer


Theorem cutmin

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

Ref Expression
Hypotheses cutmin.1 φ A s B
cutmin.2 φ X B
cutmin.3 φ y B X s y
Assertion cutmin φ A | s B = A | s X

Proof

Step Hyp Ref Expression
1 cutmin.1 φ A s B
2 cutmin.2 φ X B
3 cutmin.3 φ y B X s y
4 simpr φ x A x A
5 ssltss1 A s B A No
6 1 5 syl φ A No
7 6 sselda φ x A x No
8 slerflex x No x s x
9 7 8 syl φ x A x s x
10 breq2 y = x x s y x s x
11 10 rspcev x A x s x y A x s y
12 4 9 11 syl2anc φ x A y A x s y
13 12 ralrimiva φ x A y A x s y
14 breq1 x = X x s y X s y
15 14 rexsng X B x X x s y X s y
16 2 15 syl φ x X x s y X s y
17 16 ralbidv φ y B x X x s y y B X s y
18 3 17 mpbird φ y B x X x s y
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 20 simp3d φ A | s B s B
23 2 snssd φ X B
24 sssslt2 A | s B s B X B A | s B s X
25 22 23 24 syl2anc φ A | s B s X
26 1 13 18 21 25 cofcut1d φ A | s B = A | s X