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 madessno ⊢ ( M ‘ ( bday ‘ 𝐴 ) ) ⊆ No
2 1 sseli ⊢ ( 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) → 𝐵 ∈ No )
3 2 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐵 ∈ No )
4 negsbday ⊢ ( 𝐵 ∈ No → ( bday ‘ ( -us ‘ 𝐵 ) ) = ( bday ‘ 𝐵 ) )
5 3 4 syl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝐵 ) ) = ( bday ‘ 𝐵 ) )
6 madebdayim ⊢ ( 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) → ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ 𝐵 ) ⊆ ( bday ‘ 𝐴 ) )
8 5 7 eqsstrd ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( bday ‘ ( -us ‘ 𝐵 ) ) ⊆ ( bday ‘ 𝐴 ) )
9 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
10 3 negscld ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ∈ No )
11 madebday ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( -us ‘ 𝐵 ) ∈ No ) → ( ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( -us ‘ 𝐵 ) ) ⊆ ( bday ‘ 𝐴 ) ) )
12 9 10 11 sylancr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ ( -us ‘ 𝐵 ) ) ⊆ ( bday ‘ 𝐴 ) ) )
13 8 12 mpbird ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) )
14 onsbnd ⊢ ( ( 𝐴 ∈ Ons ∧ ( -us ‘ 𝐵 ) ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ≤s 𝐴 )
15 13 14 syldan ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐵 ) ≤s 𝐴 )
16 onsno ⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
17 16 adantr ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → 𝐴 ∈ No )
18 17 negscld ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐴 ) ∈ No )
19 18 3 slenegd ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐴 ) ≤s 𝐵 ↔ ( -us ‘ 𝐵 ) ≤s ( -us ‘ ( -us ‘ 𝐴 ) ) ) )
20 negnegs ⊢ ( 𝐴 ∈ No → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
21 17 20 syl ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ ( -us ‘ 𝐴 ) ) = 𝐴 )
22 21 breq2d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐵 ) ≤s ( -us ‘ ( -us ‘ 𝐴 ) ) ↔ ( -us ‘ 𝐵 ) ≤s 𝐴 ) )
23 19 22 bitr2d ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( ( -us ‘ 𝐵 ) ≤s 𝐴 ↔ ( -us ‘ 𝐴 ) ≤s 𝐵 ) )
24 15 23 mpbid ⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ ( M ‘ ( bday ‘ 𝐴 ) ) ) → ( -us ‘ 𝐴 ) ≤s 𝐵 )