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