Metamath Proof Explorer

Theorem sltsbday

Description: Birthday comparison rule for surreals. (Contributed by Scott Fenton, 23-Feb-2026)

Ref Expression
Hypotheses sltsbday.1 ⊢ φ → A = L | s R
sltsbday.2 ⊢ φ → B ∈ No
sltsbday.3 ⊢ φ → L ≪ s B
sltsbday.4 ⊢ φ → B ≪ s R
Assertion sltsbday ⊢ φ → bday ⁡ A ⊆ bday ⁡ B

Proof

Step Hyp Ref Expression
1 sltsbday.1 ⊢ φ → A = L | s R
2 sltsbday.2 ⊢ φ → B ∈ No
3 sltsbday.3 ⊢ φ → L ≪ s B
4 sltsbday.4 ⊢ φ → B ≪ s R
5 1 fveq2d ⊢ φ → bday ⁡ A = bday ⁡ L | s R
6 2 snn0d ⊢ φ → B ≠ ∅
7 sltstr ⊢ L ≪ s B ∧ B ≪ s R ∧ B ≠ ∅ → L ≪ s R
8 3 4 6 7 syl3anc ⊢ φ → L ≪ s R
9 cutbday ⊢ L ≪ s R → bday ⁡ L | s R = ⋂ bday x ∈ No | L ≪ s x ∧ x ≪ s R
10 8 9 syl ⊢ φ → bday ⁡ L | s R = ⋂ bday x ∈ No | L ≪ s x ∧ x ≪ s R
11 bdayfn ⊢ bday Fn No
12 ssrab2 ⊢ x ∈ No | L ≪ s x ∧ x ≪ s R ⊆ No
13 sneq ⊢ x = B → x = B
14 13 breq2d ⊢ x = B → L ≪ s x ↔ L ≪ s B
15 13 breq1d ⊢ x = B → x ≪ s R ↔ B ≪ s R
16 14 15 anbi12d ⊢ x = B → L ≪ s x ∧ x ≪ s R ↔ L ≪ s B ∧ B ≪ s R
17 3 4 jca ⊢ φ → L ≪ s B ∧ B ≪ s R
18 16 2 17 elrabd ⊢ φ → B ∈ x ∈ No | L ≪ s x ∧ x ≪ s R
19 fnfvima ⊢ bday Fn No ∧ x ∈ No | L ≪ s x ∧ x ≪ s R ⊆ No ∧ B ∈ x ∈ No | L ≪ s x ∧ x ≪ s R → bday ⁡ B ∈ bday x ∈ No | L ≪ s x ∧ x ≪ s R
20 11 12 18 19 mp3an12i ⊢ φ → bday ⁡ B ∈ bday x ∈ No | L ≪ s x ∧ x ≪ s R
21 intss1 ⊢ bday ⁡ B ∈ bday x ∈ No | L ≪ s x ∧ x ≪ s R → ⋂ bday x ∈ No | L ≪ s x ∧ x ≪ s R ⊆ bday ⁡ B
22 20 21 syl ⊢ φ → ⋂ bday x ∈ No | L ≪ s x ∧ x ≪ s R ⊆ bday ⁡ B
23 10 22 eqsstrd ⊢ φ → bday ⁡ L | s R ⊆ bday ⁡ B
24 5 23 eqsstrd ⊢ φ → bday ⁡ A ⊆ bday ⁡ B