Metamath Proof Explorer

Theorem cutbday

Description: The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021)

Ref Expression
Assertion cutbday ⊢ A ≪ s B → bday ⁡ A | s B = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B

Proof

Step Hyp Ref Expression
1 cutsval ⊢ A ≪ s B → A | s B = ι y ∈ x ∈ No | A ≪ s x ∧ x ≪ s B | bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B
2 1 eqcomd ⊢ A ≪ s B → ι y ∈ x ∈ No | A ≪ s x ∧ x ≪ s B | bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B = A | s B
3 cutcuts ⊢ A ≪ s B → A | s B ∈ No ∧ A ≪ s A | s B ∧ A | s B ≪ s B
4 sneq ⊢ x = A | s B → x = A | s B
5 4 breq2d ⊢ x = A | s B → A ≪ s x ↔ A ≪ s A | s B
6 4 breq1d ⊢ x = A | s B → x ≪ s B ↔ A | s B ≪ s B
7 5 6 anbi12d ⊢ x = A | s B → A ≪ s x ∧ x ≪ s B ↔ A ≪ s A | s B ∧ A | s B ≪ s B
8 7 elrab ⊢ A | s B ∈ x ∈ No | A ≪ s x ∧ x ≪ s B ↔ A | s B ∈ No ∧ A ≪ s A | s B ∧ A | s B ≪ s B
9 3anass ⊢ A | s B ∈ No ∧ A ≪ s A | s B ∧ A | s B ≪ s B ↔ A | s B ∈ No ∧ A ≪ s A | s B ∧ A | s B ≪ s B
10 8 9 bitr4i ⊢ A | s B ∈ x ∈ No | A ≪ s x ∧ x ≪ s B ↔ A | s B ∈ No ∧ A ≪ s A | s B ∧ A | s B ≪ s B
11 3 10 sylibr ⊢ A ≪ s B → A | s B ∈ x ∈ No | A ≪ s x ∧ x ≪ s B
12 conway ⊢ A ≪ s B → ∃! y ∈ x ∈ No | A ≪ s x ∧ x ≪ s B bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B
13 fveqeq2 ⊢ y = A | s B → bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B ↔ bday ⁡ A | s B = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B
14 13 riota2 ⊢ A | s B ∈ x ∈ No | A ≪ s x ∧ x ≪ s B ∧ ∃! y ∈ x ∈ No | A ≪ s x ∧ x ≪ s B bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B → bday ⁡ A | s B = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B ↔ ι y ∈ x ∈ No | A ≪ s x ∧ x ≪ s B | bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B = A | s B
15 11 12 14 syl2anc ⊢ A ≪ s B → bday ⁡ A | s B = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B ↔ ι y ∈ x ∈ No | A ≪ s x ∧ x ≪ s B | bday ⁡ y = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B = A | s B
16 2 15 mpbird ⊢ A ≪ s B → bday ⁡ A | s B = ⋂ bday x ∈ No | A ≪ s x ∧ x ≪ s B