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
|- ( ph -> A <
cutmax.2
|- ( ph -> X e. A )
cutmax.3
|- ( ph -> A. y e. A y <_s X )
Assertion cutmax
|- ( ph -> ( A |s B ) = ( { X } |s B ) )

Proof

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