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	$$⊢\phi \to A{\ll }_{s}B$$
	cutmin.2	$$⊢\phi \to X\in B$$
	cutmin.3	$$⊢\phi \to \forall y\in BX{\le }_{s}y$$
Assertion	cutmin	$$⊢\phi \to A{|}_{s}B=A{|}_s\left\{X\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cutmin.1	$$⊢\phi \to A{\ll }_{s}B$$
2		cutmin.2	$$⊢\phi \to X\in B$$
3		cutmin.3	$$⊢\phi \to \forall y\in BX{\le }_{s}y$$
4		simpr	$$⊢\left(\phi \wedge x\in A\right)\to x\in A$$
5		sltsss1	$$⊢A{\ll }_{s}B\to A\subseteq \mathrm{No}$$
6	1 5	syl	$$⊢\phi \to A\subseteq \mathrm{No}$$
7	6	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in \mathrm{No}$$
8		lesid	$$⊢x\in \mathrm{No}\to x{\le }_{s}x$$
9	7 8	syl	$$⊢\left(\phi \wedge x\in A\right)\to x{\le }_{s}x$$
10		breq2	$$⊢y=x\to \left(x{\le }_{s}y\leftrightarrow x{\le }_{s}x\right)$$
11	10	rspcev	$$⊢\left(x\in A\wedge x{\le }_{s}x\right)\to \exists y\in Ax{\le }_{s}y$$
12	4 9 11	syl2anc	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in Ax{\le }_{s}y$$
13	12	ralrimiva	$$⊢\phi \to \forall x\in A\exists y\in Ax{\le }_{s}y$$
14		breq1	$$⊢x=X\to \left(x{\le }_{s}y\leftrightarrow X{\le }_{s}y\right)$$
15	14	rexsng	$$⊢X\in B\to \left(\exists x\in \left\{X\right\}x{\le }_{s}y\leftrightarrow X{\le }_{s}y\right)$$
16	2 15	syl	$$⊢\phi \to \left(\exists x\in \left\{X\right\}x{\le }_{s}y\leftrightarrow X{\le }_{s}y\right)$$
17	16	ralbidv	$$⊢\phi \to \left(\forall y\in B\exists x\in \left\{X\right\}x{\le }_{s}y\leftrightarrow \forall y\in BX{\le }_{s}y\right)$$
18	3 17	mpbird	$$⊢\phi \to \forall y\in B\exists x\in \left\{X\right\}x{\le }_{s}y$$
19		cutcuts	$$⊢A{\ll }_{s}B\to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
20	1 19	syl	$$⊢\phi \to \left(A{|}_{s}B\in \mathrm{No}\wedge A{\ll }_s\left\{A{|}_{s}B\right\}\wedge \left\{A{|}_{s}B\right\}{\ll }_{s}B\right)$$
21	20	simp2d	$$⊢\phi \to A{\ll }_s\left\{A{|}_{s}B\right\}$$
22	20	simp3d	$$⊢\phi \to \left\{A{|}_{s}B\right\}{\ll }_{s}B$$
23	2	snssd	$$⊢\phi \to \left\{X\right\}\subseteq B$$
24		ssslts2	$$⊢\left(\left\{A{|}_{s}B\right\}{\ll }_{s}B\wedge \left\{X\right\}\subseteq B\right)\to \left\{A{|}_{s}B\right\}{\ll }_s\left\{X\right\}$$
25	22 23 24	syl2anc	$$⊢\phi \to \left\{A{|}_{s}B\right\}{\ll }_s\left\{X\right\}$$
26	1 13 18 21 25	cofcut1d	$$⊢\phi \to A{|}_{s}B=A{|}_s\left\{X\right\}$$