cutminmax

Description: If the left set of X has a maximum and the right set of X has a minimum, then X is equal to the cut of the maximum and the minimum. (Contributed by Scott Fenton, 23-Feb-2026)

	Ref	Expression
Hypotheses	cutminmax.1	$⊢ φ \to L \in L (X)$
	cutminmax.2	$⊢ φ \to \forall x \in L (X) x \leq_{s} L$
	cutminmax.3	$⊢ φ \to R \in R (X)$
	cutminmax.4	$⊢ φ \to \forall y \in R (X) R \leq_{s} y$
Assertion	cutminmax	$⊢ φ \to X = \{L\} \|_{s} \{R\}$

Proof

Step	Hyp	Ref	Expression
1		cutminmax.1	$⊢ φ \to L \in L (X)$
2		cutminmax.2	$⊢ φ \to \forall x \in L (X) x \leq_{s} L$
3		cutminmax.3	$⊢ φ \to R \in R (X)$
4		cutminmax.4	$⊢ φ \to \forall y \in R (X) R \leq_{s} y$
5		lltr	$⊢ L (X) ≪_{s} R (X)$
6	5	a1i	$⊢ φ \to L (X) ≪_{s} R (X)$
7		breq2	$⊢ y = b \to (R \leq_{s} y \leftrightarrow R \leq_{s} b)$
8	7	cbvralvw	$⊢ \forall y \in R (X) R \leq_{s} y \leftrightarrow \forall b \in R (X) R \leq_{s} b$
9	4 8	sylib	$⊢ φ \to \forall b \in R (X) R \leq_{s} b$
10	6 3 9	cutmin	$⊢ φ \to L (X) \|_{s} R (X) = L (X) \|_{s} \{R\}$
11		elfvdm	$⊢ L \in L (X) \to X \in dom L$
12	1 11	syl	$⊢ φ \to X \in dom L$
13		leftf	$⊢ L : No ⟶ 𝒫 No$
14	13	fdmi	$⊢ dom L = No$
15	12 14	eleqtrdi	$⊢ φ \to X \in No$
16		lrcut	$⊢ X \in No \to L (X) \|_{s} R (X) = X$
17	15 16	syl	$⊢ φ \to L (X) \|_{s} R (X) = X$
18	3	snssd	$⊢ φ \to \{R\} \subseteq R (X)$
19		ssslts2	$⊢ (L (X) ≪_{s} R (X) \land \{R\} \subseteq R (X)) \to L (X) ≪_{s} \{R\}$
20	5 18 19	sylancr	$⊢ φ \to L (X) ≪_{s} \{R\}$
21		breq1	$⊢ x = a \to (x \leq_{s} L \leftrightarrow a \leq_{s} L)$
22	21	cbvralvw	$⊢ \forall x \in L (X) x \leq_{s} L \leftrightarrow \forall a \in L (X) a \leq_{s} L$
23	2 22	sylib	$⊢ φ \to \forall a \in L (X) a \leq_{s} L$
24	20 1 23	cutmax	$⊢ φ \to L (X) \|_{s} \{R\} = \{L\} \|_{s} \{R\}$
25	10 17 24	3eqtr3d	$⊢ φ \to X = \{L\} \|_{s} \{R\}$

Metamath Proof Explorer

Theorem cutminmax

Proof