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 ⊢ A ∈ ℕ 0s → bday ⁡ A + s 1 s = suc ⁡ bday ⁡ A

Proof

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