Metamath Proof Explorer

Theorem cutbdaybnd2lim

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 cutbdaybnd2lim ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cutbdaybnd2 ⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
2 1 adantr ⊢ ( ( 𝐴 <<s 𝐵 ∧ Lim ( bday ‘ ( 𝐴 |s 𝐵 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ suc ∪ ( bday “ ( 𝐴 ∪ 𝐵 ) ) )
3 bdayfun ⊢ Fun bday
4 sltsex1 ⊢ ( 𝐴 <<s 𝐵 → 𝐴 ∈ V )
5 sltsex2 ⊢ ( 𝐴 <<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 bdayon ⊢ ( 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 “ ( 𝐴 ∪ 𝐵 ) ) )