Metamath Proof Explorer

Theorem onsbnd2

Description: The surreals of a given birthday are bounded below by the negative of that ordinal. (Contributed by Scott Fenton, 22-Feb-2026)

Ref Expression
Assertion onsbnd2 ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐴 ) ≤s 𝐵 )

Proof

Step Hyp Ref Expression
1 madeno ⊢ ( 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) → 𝐵 ∈ No )
2 1 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐵 ∈ No )
3 negbday ⊢ ( 𝐵 ∈ No → ( bday ‘ ( -us ‘ 𝐵 ) ) = ( bday ‘ 𝐵 ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝐵 ) ) = ( bday ‘ 𝐵 ) )
5 madebdayim ⊢ ( 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) )
6 5 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) )
7 4 6 eqsstrd ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝐵 ) ) ⊆ ( bday ‘ 𝐴 ) )
8 bdayon ⊢ ( bday ‘ 𝐴 ) ∈ On
9 2 negscld ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ∈ No )
10 madebday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( -us ‘ 𝐵 ) ∈ No ) → ( ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( -us ‘ 𝐵 ) ) ⊆ ( bday ‘ 𝐴 ) ) )
11 8 9 10 sylancr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( -us ‘ 𝐵 ) ) ⊆ ( bday ‘ 𝐴 ) ) )
12 7 11 mpbird ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) )
13 onsbnd ⊢ ( ( 𝐴 ∈ Ons ∧ ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ≤s 𝐴 )
14 12 13 syldan ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ≤s 𝐴 )
15 onno ⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
16 15 adantr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 ∈ No )
17 16 negscld ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐴 ) ∈ No )
18 17 2 lenegsd ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐴 ) ≤s 𝐵 ↔ ( -us ‘ 𝐵 ) ≤s ( -us ‘ ( -us ‘ 𝐴 ) ) ) )
19 negnegs ⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
20 16 19 syl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
21 20 breq2d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐵 ) ≤s ( -us ‘ ( -us ‘ 𝐴 ) ) ↔ ( -us ‘ 𝐵 ) ≤s 𝐴 ) )
22 18 21 bitr2d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐵 ) ≤s 𝐴 ↔ ( -us ‘ 𝐴 ) ≤s 𝐵 ) )
23 14 22 mpbid ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐴 ) ≤s 𝐵 )