Metamath Proof Explorer

Theorem bdayn0p1

Description: The birthday of A +s 1s is the successor of the birthday of A when A is a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025)

Ref Expression
Assertion bdayn0p1 ( 𝐴 ∈ ℕ0s → ( bday ‘ ( 𝐴 +s 1s ) ) = suc ( bday ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 n0scut2 ⊢ ( 𝐴 ∈ ℕ0s → ( 𝐴 +s 1s ) = ( { 𝐴 } |s ∅ ) )
2 1 fveq2d ⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ ( 𝐴 +s 1s ) ) = ( bday ‘ ( { 𝐴 } |s ∅ ) ) )
3 n0sno ⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ No )
4 snelpwi ⊢ ( 𝐴 ∈ No → { 𝐴 } ∈ 𝒫 No )
5 nulssgt ⊢ ( { 𝐴 } ∈ 𝒫 No → { 𝐴 } <<s ∅ )
6 3 4 5 3syl ⊢ ( 𝐴 ∈ ℕ0s → { 𝐴 } <<s ∅ )
7 un0 ⊢ ( { 𝐴 } ∪ ∅ ) = { 𝐴 }
8 7 imaeq2i ⊢ ( bday “ ( { 𝐴 } ∪ ∅ ) ) = ( bday “ { 𝐴 } )
9 bdayfn ⊢ bday Fn No
10 9 a1i ⊢ ( 𝐴 ∈ ℕ0s → bday Fn No )
11 10 3 fnimasnd ⊢ ( 𝐴 ∈ ℕ0s → ( bday “ { 𝐴 } ) = { ( bday ‘ 𝐴 ) } )
12 ssun2 ⊢ { ( bday ‘ 𝐴 ) } ⊆ ( ( bday ‘ 𝐴 ) ∪ { ( bday ‘ 𝐴 ) } )
13 df-suc ⊢ suc ( bday ‘ 𝐴 ) = ( ( bday ‘ 𝐴 ) ∪ { ( bday ‘ 𝐴 ) } )
14 12 13 sseqtrri ⊢ { ( bday ‘ 𝐴 ) } ⊆ suc ( bday ‘ 𝐴 )
15 11 14 eqsstrdi ⊢ ( 𝐴 ∈ ℕ0s → ( bday “ { 𝐴 } ) ⊆ suc ( bday ‘ 𝐴 ) )
16 8 15 eqsstrid ⊢ ( 𝐴 ∈ ℕ0s → ( bday “ ( { 𝐴 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝐴 ) )
17 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
18 onsuc ⊢ ( ( bday ‘ 𝐴 ) ∈ On → suc ( bday ‘ 𝐴 ) ∈ On )
19 17 18 ax-mp ⊢ suc ( bday ‘ 𝐴 ) ∈ On
20 scutbdaybnd ⊢ ( ( { 𝐴 } <<s ∅ ∧ suc ( bday ‘ 𝐴 ) ∈ On ∧ ( bday “ ( { 𝐴 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝐴 ) ) → ( bday ‘ ( { 𝐴 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝐴 ) )
21 19 20 mp3an2 ⊢ ( ( { 𝐴 } <<s ∅ ∧ ( bday “ ( { 𝐴 } ∪ ∅ ) ) ⊆ suc ( bday ‘ 𝐴 ) ) → ( bday ‘ ( { 𝐴 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝐴 ) )
22 6 16 21 syl2anc ⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ ( { 𝐴 } |s ∅ ) ) ⊆ suc ( bday ‘ 𝐴 ) )
23 ssltsep ⊢ ( { 𝐴 } <<s { 𝑧 } → ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝑧 } 𝑥 <s 𝑦 )
24 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑦 ) )
25 24 ralbidv ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ { 𝑧 } 𝑥 <s 𝑦 ↔ ∀ 𝑦 ∈ { 𝑧 } 𝐴 <s 𝑦 ) )
26 vex ⊢ 𝑧 ∈ V
27 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐴 <s 𝑦 ↔ 𝐴 <s 𝑧 ) )
28 26 27 ralsn ⊢ ( ∀ 𝑦 ∈ { 𝑧 } 𝐴 <s 𝑦 ↔ 𝐴 <s 𝑧 )
29 25 28 bitrdi ⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ { 𝑧 } 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑧 ) )
30 29 ralsng ⊢ ( 𝐴 ∈ ℕ0s → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝑧 } 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑧 ) )
31 30 adantr ⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑧 ∈ No ) → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝑧 } 𝑥 <s 𝑦 ↔ 𝐴 <s 𝑧 ) )
32 n0ons ⊢ ( 𝐴 ∈ ℕ0s → 𝐴 ∈ Ons )
33 onnolt ⊢ ( ( 𝐴 ∈ Ons ∧ 𝑧 ∈ No ∧ 𝐴 <s 𝑧 ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) )
34 32 33 syl3an1 ⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑧 ∈ No ∧ 𝐴 <s 𝑧 ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) )
35 34 3expia ⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑧 ∈ No ) → ( 𝐴 <s 𝑧 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
36 31 35 sylbid ⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑧 ∈ No ) → ( ∀ 𝑥 ∈ { 𝐴 } ∀ 𝑦 ∈ { 𝑧 } 𝑥 <s 𝑦 → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
37 23 36 syl5 ⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑧 ∈ No ) → ( { 𝐴 } <<s { 𝑧 } → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
38 37 adantrd ⊢ ( ( 𝐴 ∈ ℕ0s ∧ 𝑧 ∈ No ) → ( ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
39 38 ralrimiva ⊢ ( 𝐴 ∈ ℕ0s → ∀ 𝑧 ∈ No ( ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
40 ssint ⊢ ( suc ( bday ‘ 𝐴 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) ↔ ∀ 𝑦 ∈ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) suc ( bday ‘ 𝐴 ) ⊆ 𝑦 )
41 ssrab2 ⊢ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ⊆ No
42 sseq2 ⊢ ( 𝑦 = ( bday ‘ 𝑧 ) → ( suc ( bday ‘ 𝐴 ) ⊆ 𝑦 ↔ suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑧 ) ) )
43 42 ralima ⊢ ( ( bday Fn No ∧ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ⊆ No ) → ( ∀ 𝑦 ∈ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) suc ( bday ‘ 𝐴 ) ⊆ 𝑦 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑧 ) ) )
44 9 41 43 mp2an ⊢ ( ∀ 𝑦 ∈ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) suc ( bday ‘ 𝐴 ) ⊆ 𝑦 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑧 ) )
45 bdayelon ⊢ ( bday ‘ 𝑧 ) ∈ On
46 17 45 onsucssi ⊢ ( ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ↔ suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑧 ) )
47 46 ralbii ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑧 ) )
48 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
49 48 breq2d ⊢ ( 𝑥 = 𝑧 → ( { 𝐴 } <<s { 𝑥 } ↔ { 𝐴 } <<s { 𝑧 } ) )
50 48 breq1d ⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } <<s ∅ ↔ { 𝑧 } <<s ∅ ) )
51 49 50 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) ↔ ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) ) )
52 51 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ No ( ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
53 47 52 bitr3i ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ No ( ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
54 44 53 bitri ⊢ ( ∀ 𝑦 ∈ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) suc ( bday ‘ 𝐴 ) ⊆ 𝑦 ↔ ∀ 𝑧 ∈ No ( ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
55 40 54 bitri ⊢ ( suc ( bday ‘ 𝐴 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) ↔ ∀ 𝑧 ∈ No ( ( { 𝐴 } <<s { 𝑧 } ∧ { 𝑧 } <<s ∅ ) → ( bday ‘ 𝐴 ) ∈ ( bday ‘ 𝑧 ) ) )
56 39 55 sylibr ⊢ ( 𝐴 ∈ ℕ0s → suc ( bday ‘ 𝐴 ) ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) )
57 scutbday ⊢ ( { 𝐴 } <<s ∅ → ( bday ‘ ( { 𝐴 } |s ∅ ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) )
58 6 57 syl ⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ ( { 𝐴 } |s ∅ ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 𝐴 } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) )
59 56 58 sseqtrrd ⊢ ( 𝐴 ∈ ℕ0s → suc ( bday ‘ 𝐴 ) ⊆ ( bday ‘ ( { 𝐴 } |s ∅ ) ) )
60 22 59 eqssd ⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ ( { 𝐴 } |s ∅ ) ) = suc ( bday ‘ 𝐴 ) )
61 2 60 eqtrd ⊢ ( 𝐴 ∈ ℕ0s → ( bday ‘ ( 𝐴 +s 1s ) ) = suc ( bday ‘ 𝐴 ) )