Metamath Proof Explorer


Theorem scutbdaybnd2lim

Description: An upper bound on the birthday of a surreal cut when it is a limit birthday. (Contributed by Scott Fenton, 7-Aug-2024)

Ref Expression
Assertion scutbdaybnd2lim ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday “ ( 𝐴𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 scutbdaybnd2 ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ( bday “ ( 𝐴𝐵 ) ) )
2 1 adantr ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ( bday “ ( 𝐴𝐵 ) ) )
3 bdayfun Fun bday
4 ssltex1 ( 𝐴 <<s 𝐵𝐴 ∈ V )
5 ssltex2 ( 𝐴 <<s 𝐵𝐵 ∈ V )
6 unexg ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴𝐵 ) ∈ V )
7 4 5 6 syl2anc ( 𝐴 <<s 𝐵 → ( 𝐴𝐵 ) ∈ V )
8 funimaexg ( ( Fun bday ∧ ( 𝐴𝐵 ) ∈ V ) → ( bday “ ( 𝐴𝐵 ) ) ∈ V )
9 3 7 8 sylancr ( 𝐴 <<s 𝐵 → ( bday “ ( 𝐴𝐵 ) ) ∈ V )
10 9 uniexd ( 𝐴 <<s 𝐵 ( bday “ ( 𝐴𝐵 ) ) ∈ V )
11 10 adantr ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday “ ( 𝐴𝐵 ) ) ∈ V )
12 nlimsucg ( ( bday “ ( 𝐴𝐵 ) ) ∈ V → ¬ Lim suc ( bday “ ( 𝐴𝐵 ) ) )
13 11 12 syl ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ¬ Lim suc ( bday “ ( 𝐴𝐵 ) ) )
14 limeq ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = suc ( bday “ ( 𝐴𝐵 ) ) → ( Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ↔ Lim suc ( bday “ ( 𝐴𝐵 ) ) ) )
15 14 biimpcd ( Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = suc ( bday “ ( 𝐴𝐵 ) ) → Lim suc ( bday “ ( 𝐴𝐵 ) ) ) )
16 15 adantl ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = suc ( bday “ ( 𝐴𝐵 ) ) → Lim suc ( bday “ ( 𝐴𝐵 ) ) ) )
17 13 16 mtod ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ¬ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = suc ( bday “ ( 𝐴𝐵 ) ) )
18 17 neqned ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ suc ( bday “ ( 𝐴𝐵 ) ) )
19 bdayelon ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On
20 19 onordi Ord ( bday ‘ ( 𝐴 |s 𝐵 ) )
21 imassrn ( bday “ ( 𝐴𝐵 ) ) ⊆ ran bday
22 bdayrn ran bday = On
23 21 22 sseqtri ( bday “ ( 𝐴𝐵 ) ) ⊆ On
24 ssorduni ( ( bday “ ( 𝐴𝐵 ) ) ⊆ On → Ord ( bday “ ( 𝐴𝐵 ) ) )
25 23 24 ax-mp Ord ( bday “ ( 𝐴𝐵 ) )
26 ordsuc ( Ord ( bday “ ( 𝐴𝐵 ) ) ↔ Ord suc ( bday “ ( 𝐴𝐵 ) ) )
27 25 26 mpbi Ord suc ( bday “ ( 𝐴𝐵 ) )
28 ordelssne ( ( Ord ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∧ Ord suc ( bday “ ( 𝐴𝐵 ) ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ suc ( bday “ ( 𝐴𝐵 ) ) ↔ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ( bday “ ( 𝐴𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ suc ( bday “ ( 𝐴𝐵 ) ) ) ) )
29 20 27 28 mp2an ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ suc ( bday “ ( 𝐴𝐵 ) ) ↔ ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ( bday “ ( 𝐴𝐵 ) ) ∧ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ≠ suc ( bday “ ( 𝐴𝐵 ) ) ) )
30 2 18 29 sylanbrc ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ suc ( bday “ ( 𝐴𝐵 ) ) )
31 19 a1i ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On )
32 ordsssuc ( ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ On ∧ Ord ( bday “ ( 𝐴𝐵 ) ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday “ ( 𝐴𝐵 ) ) ↔ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ suc ( bday “ ( 𝐴𝐵 ) ) ) )
33 31 25 32 sylancl ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday “ ( 𝐴𝐵 ) ) ↔ ( bday ‘ ( 𝐴 |s 𝐵 ) ) ∈ suc ( bday “ ( 𝐴𝐵 ) ) ) )
34 30 33 mpbird ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday “ ( 𝐴𝐵 ) ) )