| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . 3
⊢ (𝑚 = 0s → ( bday ‘𝑚) = ( bday
‘ 0s )) | 
| 2 | 1 | eleq1d 2825 | . 2
⊢ (𝑚 = 0s → (( bday ‘𝑚) ∈ ω ↔ ( bday ‘ 0s ) ∈
ω)) | 
| 3 |  | fveq2 6905 | . . 3
⊢ (𝑚 = 𝑛 → ( bday
‘𝑚) = ( bday ‘𝑛)) | 
| 4 | 3 | eleq1d 2825 | . 2
⊢ (𝑚 = 𝑛 → (( bday
‘𝑚) ∈
ω ↔ ( bday ‘𝑛) ∈ ω)) | 
| 5 |  | fveq2 6905 | . . 3
⊢ (𝑚 = (𝑛 +s 1s ) → ( bday ‘𝑚) = ( bday
‘(𝑛
+s 1s ))) | 
| 6 | 5 | eleq1d 2825 | . 2
⊢ (𝑚 = (𝑛 +s 1s ) → (( bday ‘𝑚) ∈ ω ↔ ( bday ‘(𝑛 +s 1s )) ∈
ω)) | 
| 7 |  | fveq2 6905 | . . 3
⊢ (𝑚 = 𝐴 → ( bday
‘𝑚) = ( bday ‘𝐴)) | 
| 8 | 7 | eleq1d 2825 | . 2
⊢ (𝑚 = 𝐴 → (( bday
‘𝑚) ∈
ω ↔ ( bday ‘𝐴) ∈ ω)) | 
| 9 |  | bday0s 27874 | . . 3
⊢ ( bday ‘ 0s ) = ∅ | 
| 10 |  | peano1 7911 | . . 3
⊢ ∅
∈ ω | 
| 11 | 9, 10 | eqeltri 2836 | . 2
⊢ ( bday ‘ 0s ) ∈
ω | 
| 12 |  | peano2n0s 28336 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (𝑛 +s
1s ) ∈ ℕ0s) | 
| 13 |  | n0scut 28339 | . . . . . . . . 9
⊢ ((𝑛 +s 1s )
∈ ℕ0s → (𝑛 +s 1s ) = ({((𝑛 +s 1s )
-s 1s )} |s ∅)) | 
| 14 | 12, 13 | syl 17 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ (𝑛 +s
1s ) = ({((𝑛
+s 1s ) -s 1s )} |s
∅)) | 
| 15 |  | n0sno 28329 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0s
→ 𝑛 ∈  No ) | 
| 16 |  | 1sno 27873 | . . . . . . . . . . 11
⊢ 
1s ∈  No | 
| 17 |  | pncans 28103 | . . . . . . . . . . 11
⊢ ((𝑛 ∈ 
No  ∧ 1s ∈  No ) →
((𝑛 +s
1s ) -s 1s ) = 𝑛) | 
| 18 | 15, 16, 17 | sylancl 586 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ ((𝑛 +s
1s ) -s 1s ) = 𝑛) | 
| 19 | 18 | sneqd 4637 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ {((𝑛 +s
1s ) -s 1s )} = {𝑛}) | 
| 20 | 19 | oveq1d 7447 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ ({((𝑛 +s
1s ) -s 1s )} |s ∅) = ({𝑛} |s ∅)) | 
| 21 | 14, 20 | eqtrd 2776 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ (𝑛 +s
1s ) = ({𝑛} |s
∅)) | 
| 22 | 21 | fveq2d 6909 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘(𝑛 +s 1s )) = ( bday ‘({𝑛} |s ∅))) | 
| 23 |  | snelpwi 5447 | . . . . . . . 8
⊢ (𝑛 ∈ 
No  → {𝑛}
∈ 𝒫  No ) | 
| 24 |  | nulssgt 27844 | . . . . . . . 8
⊢ ({𝑛} ∈ 𝒫  No  → {𝑛} <<s ∅) | 
| 25 | 15, 23, 24 | 3syl 18 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ {𝑛} <<s
∅) | 
| 26 |  | un0 4393 | . . . . . . . . . 10
⊢ ({𝑛} ∪ ∅) = {𝑛} | 
| 27 | 26 | imaeq2i 6075 | . . . . . . . . 9
⊢ ( bday  “ ({𝑛} ∪ ∅)) = (
bday  “ {𝑛}) | 
| 28 |  | bdayfn 27819 | . . . . . . . . . 10
⊢  bday  Fn  No | 
| 29 |  | fnsnfv 6987 | . . . . . . . . . 10
⊢ (( bday  Fn  No  ∧ 𝑛 ∈ 
No ) → {( bday ‘𝑛)} = (
bday  “ {𝑛})) | 
| 30 | 28, 15, 29 | sylancr 587 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ {( bday ‘𝑛)} = ( bday 
“ {𝑛})) | 
| 31 | 27, 30 | eqtr4id 2795 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ ( bday  “ ({𝑛} ∪ ∅)) = {(
bday ‘𝑛)}) | 
| 32 |  | fvex 6918 | . . . . . . . . . 10
⊢ ( bday ‘𝑛) ∈ V | 
| 33 | 32 | sucid 6465 | . . . . . . . . 9
⊢ ( bday ‘𝑛) ∈ suc ( bday
‘𝑛) | 
| 34 |  | snssi 4807 | . . . . . . . . 9
⊢ (( bday ‘𝑛) ∈ suc ( bday
‘𝑛) →
{( bday ‘𝑛)} ⊆ suc ( bday
‘𝑛)) | 
| 35 | 33, 34 | ax-mp 5 | . . . . . . . 8
⊢ {( bday ‘𝑛)} ⊆ suc ( bday
‘𝑛) | 
| 36 | 31, 35 | eqsstrdi 4027 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ ( bday  “ ({𝑛} ∪ ∅)) ⊆ suc ( bday ‘𝑛)) | 
| 37 |  | bdayelon 27822 | . . . . . . . . 9
⊢ ( bday ‘𝑛) ∈ On | 
| 38 | 37 | onsuci 7860 | . . . . . . . 8
⊢ suc
( bday ‘𝑛) ∈ On | 
| 39 |  | scutbdaybnd 27861 | . . . . . . . 8
⊢ (({𝑛} <<s ∅ ∧ suc
( bday ‘𝑛) ∈ On ∧ (
bday  “ ({𝑛}
∪ ∅)) ⊆ suc ( bday ‘𝑛)) → ( bday ‘({𝑛} |s ∅)) ⊆ suc ( bday ‘𝑛)) | 
| 40 | 38, 39 | mp3an2 1450 | . . . . . . 7
⊢ (({𝑛} <<s ∅ ∧ ( bday  “ ({𝑛} ∪ ∅)) ⊆ suc ( bday ‘𝑛)) → ( bday
‘({𝑛} |s
∅)) ⊆ suc ( bday ‘𝑛)) | 
| 41 | 25, 36, 40 | syl2anc 584 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘({𝑛} |s ∅)) ⊆ suc ( bday ‘𝑛)) | 
| 42 | 22, 41 | eqsstrd 4017 | . . . . 5
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘(𝑛 +s 1s )) ⊆ suc
( bday ‘𝑛)) | 
| 43 |  | bdayelon 27822 | . . . . . 6
⊢ ( bday ‘(𝑛 +s 1s )) ∈
On | 
| 44 |  | onsssuc 6473 | . . . . . 6
⊢ ((( bday ‘(𝑛 +s 1s )) ∈ On
∧ suc ( bday ‘𝑛) ∈ On) → ((
bday ‘(𝑛
+s 1s )) ⊆ suc ( bday
‘𝑛) ↔
( bday ‘(𝑛 +s 1s )) ∈ suc
suc ( bday ‘𝑛))) | 
| 45 | 43, 38, 44 | mp2an 692 | . . . . 5
⊢ (( bday ‘(𝑛 +s 1s )) ⊆ suc
( bday ‘𝑛) ↔ ( bday
‘(𝑛
+s 1s )) ∈ suc suc ( bday
‘𝑛)) | 
| 46 | 42, 45 | sylib 218 | . . . 4
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘(𝑛 +s 1s )) ∈ suc
suc ( bday ‘𝑛)) | 
| 47 |  | peano2 7913 | . . . . 5
⊢ (( bday ‘𝑛) ∈ ω → suc ( bday ‘𝑛) ∈ ω) | 
| 48 |  | peano2 7913 | . . . . 5
⊢ (suc
( bday ‘𝑛) ∈ ω → suc suc ( bday ‘𝑛) ∈ ω) | 
| 49 | 47, 48 | syl 17 | . . . 4
⊢ (( bday ‘𝑛) ∈ ω → suc suc ( bday ‘𝑛) ∈ ω) | 
| 50 |  | elnn 7899 | . . . 4
⊢ ((( bday ‘(𝑛 +s 1s )) ∈ suc
suc ( bday ‘𝑛) ∧ suc suc ( bday
‘𝑛) ∈
ω) → ( bday ‘(𝑛 +s 1s )) ∈
ω) | 
| 51 | 46, 49, 50 | syl2an 596 | . . 3
⊢ ((𝑛 ∈ ℕ0s
∧ ( bday ‘𝑛) ∈ ω) → ( bday ‘(𝑛 +s 1s )) ∈
ω) | 
| 52 | 51 | ex 412 | . 2
⊢ (𝑛 ∈ ℕ0s
→ (( bday ‘𝑛) ∈ ω → ( bday ‘(𝑛 +s 1s )) ∈
ω)) | 
| 53 | 2, 4, 6, 8, 11, 52 | n0sind 28338 | 1
⊢ (𝐴 ∈ ℕ0s
→ ( bday ‘𝐴) ∈ ω) |