Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  scutbdaybnd Structured version   Visualization version   GIF version

Theorem scutbdaybnd 32198
 Description: An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Dec-2021.)
Assertion
Ref Expression
scutbdaybnd (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ( bday “ (𝐴𝐵)))

Proof of Theorem scutbdaybnd
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etasslt 32197 . 2 (𝐴 <<s 𝐵 → ∃𝑥 No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))
2 scutbday 32190 . . . . . 6 (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
32adantr 472 . . . . 5 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → ( bday ‘(𝐴 |s 𝐵)) = ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
4 bdayfn 32166 . . . . . . 7 bday Fn No
5 ssrab2 3816 . . . . . . 7 {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No
6 simprl 811 . . . . . . . 8 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → 𝑥 No )
7 simprr1 1249 . . . . . . . . 9 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → 𝐴 <<s {𝑥})
8 simprr2 1251 . . . . . . . . 9 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → {𝑥} <<s 𝐵)
97, 8jca 555 . . . . . . . 8 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵))
10 sneq 4319 . . . . . . . . . . 11 (𝑦 = 𝑥 → {𝑦} = {𝑥})
1110breq2d 4804 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝐴 <<s {𝑦} ↔ 𝐴 <<s {𝑥}))
1210breq1d 4802 . . . . . . . . . 10 (𝑦 = 𝑥 → ({𝑦} <<s 𝐵 ↔ {𝑥} <<s 𝐵))
1311, 12anbi12d 749 . . . . . . . . 9 (𝑦 = 𝑥 → ((𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵) ↔ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
1413elrab 3492 . . . . . . . 8 (𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ↔ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵)))
156, 9, 14sylanbrc 701 . . . . . . 7 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → 𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)})
16 fnfvima 6647 . . . . . . 7 (( bday Fn No ∧ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)} ⊆ No 𝑥 ∈ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday 𝑥) ∈ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
174, 5, 15, 16mp3an12i 1565 . . . . . 6 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → ( bday 𝑥) ∈ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}))
18 intss1 4632 . . . . . 6 (( bday 𝑥) ∈ ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) → ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday 𝑥))
1917, 18syl 17 . . . . 5 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → ( bday “ {𝑦 No ∣ (𝐴 <<s {𝑦} ∧ {𝑦} <<s 𝐵)}) ⊆ ( bday 𝑥))
203, 19eqsstrd 3768 . . . 4 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ ( bday 𝑥))
21 simprr3 1253 . . . 4 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵)))
2220, 21sstrd 3742 . . 3 ((𝐴 <<s 𝐵 ∧ (𝑥 No ∧ (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ( bday “ (𝐴𝐵)))
2322rexlimdvaa 3158 . 2 (𝐴 <<s 𝐵 → (∃𝑥 No (𝐴 <<s {𝑥} ∧ {𝑥} <<s 𝐵 ∧ ( bday 𝑥) ⊆ suc ( bday “ (𝐴𝐵))) → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ( bday “ (𝐴𝐵))))
241, 23mpd 15 1 (𝐴 <<s 𝐵 → ( bday ‘(𝐴 |s 𝐵)) ⊆ suc ( bday “ (𝐴𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1620   ∈ wcel 2127  ∃wrex 3039  {crab 3042   ∪ cun 3701   ⊆ wss 3703  {csn 4309  ∪ cuni 4576  ∩ cint 4615   class class class wbr 4792   “ cima 5257  suc csuc 5874   Fn wfn 6032  ‘cfv 6037  (class class class)co 6801   No csur 32070   bday cbday 32072   <
 Copyright terms: Public domain W3C validator