Metamath Proof Explorer

Theorem scutbday

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 scutbday ⊢A≪sB→bday⁡A|sB=⋂bdayx∈No|A≪sx∧x≪sB

Proof

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