| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑚 = 0s →
(2s↑s𝑚) = (2s↑s
0s )) | 
| 2 |  | 2sno 28403 | . . . . . . . . 9
⊢
2s ∈  No | 
| 3 |  | exps0 28410 | . . . . . . . . 9
⊢
(2s ∈  No  →
(2s↑s 0s ) = 1s
) | 
| 4 | 2, 3 | ax-mp 5 | . . . . . . . 8
⊢
(2s↑s 0s ) =
1s | 
| 5 | 1, 4 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑚 = 0s →
(2s↑s𝑚) = 1s ) | 
| 6 | 5 | oveq2d 7447 | . . . . . 6
⊢ (𝑚 = 0s → (
1s /su (2s↑s𝑚)) = ( 1s
/su 1s )) | 
| 7 |  | 1sno 27872 | . . . . . . 7
⊢ 
1s ∈  No | 
| 8 |  | divs1 28229 | . . . . . . 7
⊢ (
1s ∈  No  → ( 1s
/su 1s ) = 1s ) | 
| 9 | 7, 8 | ax-mp 5 | . . . . . 6
⊢ (
1s /su 1s ) =
1s | 
| 10 | 6, 9 | eqtrdi 2793 | . . . . 5
⊢ (𝑚 = 0s → (
1s /su (2s↑s𝑚)) = 1s
) | 
| 11 | 10 | fveq2d 6910 | . . . 4
⊢ (𝑚 = 0s → ( bday ‘( 1s /su
(2s↑s𝑚))) = ( bday
‘ 1s )) | 
| 12 |  | bday1s 27876 | . . . 4
⊢ ( bday ‘ 1s ) =
1o | 
| 13 | 11, 12 | eqtrdi 2793 | . . 3
⊢ (𝑚 = 0s → ( bday ‘( 1s /su
(2s↑s𝑚))) = 1o) | 
| 14 | 13 | eleq1d 2826 | . 2
⊢ (𝑚 = 0s → (( bday ‘( 1s /su
(2s↑s𝑚))) ∈ ω ↔ 1o
∈ ω)) | 
| 15 |  | oveq2 7439 | . . . . 5
⊢ (𝑚 = 𝑛 → (2s↑s𝑚) =
(2s↑s𝑛)) | 
| 16 | 15 | oveq2d 7447 | . . . 4
⊢ (𝑚 = 𝑛 → ( 1s /su
(2s↑s𝑚)) = ( 1s /su
(2s↑s𝑛))) | 
| 17 | 16 | fveq2d 6910 | . . 3
⊢ (𝑚 = 𝑛 → ( bday
‘( 1s /su
(2s↑s𝑚))) = ( bday
‘( 1s /su
(2s↑s𝑛)))) | 
| 18 | 17 | eleq1d 2826 | . 2
⊢ (𝑚 = 𝑛 → (( bday
‘( 1s /su
(2s↑s𝑚))) ∈ ω ↔ ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω)) | 
| 19 |  | oveq2 7439 | . . . . 5
⊢ (𝑚 = (𝑛 +s 1s ) →
(2s↑s𝑚) = (2s↑s(𝑛 +s 1s
))) | 
| 20 | 19 | oveq2d 7447 | . . . 4
⊢ (𝑚 = (𝑛 +s 1s ) → (
1s /su (2s↑s𝑚)) = ( 1s
/su (2s↑s(𝑛 +s 1s
)))) | 
| 21 | 20 | fveq2d 6910 | . . 3
⊢ (𝑚 = (𝑛 +s 1s ) → ( bday ‘( 1s /su
(2s↑s𝑚))) = ( bday
‘( 1s /su
(2s↑s(𝑛 +s 1s
))))) | 
| 22 | 21 | eleq1d 2826 | . 2
⊢ (𝑚 = (𝑛 +s 1s ) → (( bday ‘( 1s /su
(2s↑s𝑚))) ∈ ω ↔ ( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) | 
| 23 |  | oveq2 7439 | . . . . 5
⊢ (𝑚 = 𝑁 →
(2s↑s𝑚) = (2s↑s𝑁)) | 
| 24 | 23 | oveq2d 7447 | . . . 4
⊢ (𝑚 = 𝑁 → ( 1s /su
(2s↑s𝑚)) = ( 1s /su
(2s↑s𝑁))) | 
| 25 | 24 | fveq2d 6910 | . . 3
⊢ (𝑚 = 𝑁 → ( bday
‘( 1s /su
(2s↑s𝑚))) = ( bday
‘( 1s /su
(2s↑s𝑁)))) | 
| 26 | 25 | eleq1d 2826 | . 2
⊢ (𝑚 = 𝑁 → (( bday
‘( 1s /su
(2s↑s𝑚))) ∈ ω ↔ ( bday ‘( 1s /su
(2s↑s𝑁))) ∈ ω)) | 
| 27 |  | 1onn 8678 | . 2
⊢
1o ∈ ω | 
| 28 |  | cutpw2 28417 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su
(2s↑s(𝑛 +s 1s ))) = ({
0s } |s {( 1s /su
(2s↑s𝑛))})) | 
| 29 | 28 | fveq2d 6910 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘( 1s
/su (2s↑s(𝑛 +s 1s )))) = ( bday ‘({ 0s } |s {( 1s
/su (2s↑s𝑛))}))) | 
| 30 |  | 0sno 27871 | . . . . . . . . 9
⊢ 
0s ∈  No | 
| 31 | 30 | a1i 11 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ 0s ∈  No ) | 
| 32 | 7 | a1i 11 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ 1s ∈  No ) | 
| 33 |  | expscl 28413 | . . . . . . . . . 10
⊢
((2s ∈  No  ∧ 𝑛 ∈ ℕ0s)
→ (2s↑s𝑛) ∈  No
) | 
| 34 | 2, 33 | mpan 690 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s𝑛) ∈  No
) | 
| 35 |  | 2ne0s 28404 | . . . . . . . . . 10
⊢
2s ≠ 0s | 
| 36 |  | expsne0 28414 | . . . . . . . . . 10
⊢
((2s ∈  No  ∧
2s ≠ 0s ∧ 𝑛 ∈ ℕ0s) →
(2s↑s𝑛) ≠ 0s ) | 
| 37 | 2, 35, 36 | mp3an12 1453 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (2s↑s𝑛) ≠ 0s ) | 
| 38 | 32, 34, 37 | divscld 28248 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ ( 1s /su (2s↑s𝑛)) ∈ 
No ) | 
| 39 |  | muls02 28167 | . . . . . . . . . . 11
⊢
((2s↑s𝑛) ∈  No 
→ ( 0s ·s
(2s↑s𝑛)) = 0s ) | 
| 40 | 34, 39 | syl 17 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ ( 0s ·s
(2s↑s𝑛)) = 0s ) | 
| 41 |  | 0slt1s 27874 | . . . . . . . . . 10
⊢ 
0s <s 1s | 
| 42 | 40, 41 | eqbrtrdi 5182 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ ( 0s ·s
(2s↑s𝑛)) <s 1s ) | 
| 43 |  | 2nns 28402 | . . . . . . . . . . . 12
⊢
2s ∈ ℕs | 
| 44 |  | nnsgt0 28342 | . . . . . . . . . . . 12
⊢
(2s ∈ ℕs → 0s <s
2s) | 
| 45 | 43, 44 | ax-mp 5 | . . . . . . . . . . 11
⊢ 
0s <s 2s | 
| 46 |  | expsgt0 28415 | . . . . . . . . . . 11
⊢
((2s ∈  No  ∧ 𝑛 ∈ ℕ0s
∧ 0s <s 2s) → 0s <s
(2s↑s𝑛)) | 
| 47 | 2, 45, 46 | mp3an13 1454 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ 0s <s (2s↑s𝑛)) | 
| 48 | 31, 32, 34, 47 | sltmuldivd 28253 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (( 0s ·s
(2s↑s𝑛)) <s 1s ↔ 0s
<s ( 1s /su (2s↑s𝑛)))) | 
| 49 | 42, 48 | mpbid 232 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ 0s <s ( 1s /su
(2s↑s𝑛))) | 
| 50 | 31, 38, 49 | ssltsn 27837 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ { 0s } <<s {( 1s /su
(2s↑s𝑛))}) | 
| 51 |  | suc0 6459 | . . . . . . . . . . . 12
⊢ suc
∅ = {∅} | 
| 52 |  | bday0s 27873 | . . . . . . . . . . . . 13
⊢ ( bday ‘ 0s ) = ∅ | 
| 53 | 52 | sneqi 4637 | . . . . . . . . . . . 12
⊢ {( bday ‘ 0s )} =
{∅} | 
| 54 |  | bdayfn 27818 | . . . . . . . . . . . . 13
⊢  bday  Fn  No | 
| 55 |  | fnsnfv 6988 | . . . . . . . . . . . . 13
⊢ (( bday  Fn  No  ∧
0s ∈  No ) → {( bday ‘ 0s )} = (
bday  “ { 0s })) | 
| 56 | 54, 30, 55 | mp2an 692 | . . . . . . . . . . . 12
⊢ {( bday ‘ 0s )} = (
bday  “ { 0s }) | 
| 57 | 51, 53, 56 | 3eqtr2i 2771 | . . . . . . . . . . 11
⊢ suc
∅ = ( bday  “ { 0s
}) | 
| 58 | 57 | a1i 11 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ suc ∅ = ( bday  “ {
0s })) | 
| 59 |  | fnsnfv 6988 | . . . . . . . . . . . 12
⊢ (( bday  Fn  No  ∧ (
1s /su (2s↑s𝑛)) ∈ 
No ) → {( bday ‘( 1s
/su (2s↑s𝑛)))} = ( bday 
“ {( 1s /su
(2s↑s𝑛))})) | 
| 60 | 54, 59 | mpan 690 | . . . . . . . . . . 11
⊢ ((
1s /su (2s↑s𝑛)) ∈ 
No  → {( bday ‘( 1s
/su (2s↑s𝑛)))} = ( bday 
“ {( 1s /su
(2s↑s𝑛))})) | 
| 61 | 38, 60 | syl 17 | . . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0s
→ {( bday ‘( 1s
/su (2s↑s𝑛)))} = ( bday 
“ {( 1s /su
(2s↑s𝑛))})) | 
| 62 | 58, 61 | uneq12d 4169 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0s
→ (suc ∅ ∪ {( bday ‘(
1s /su (2s↑s𝑛)))}) = ((
bday  “ { 0s }) ∪ ( bday
 “ {( 1s /su
(2s↑s𝑛))}))) | 
| 63 |  | imaundi 6169 | . . . . . . . . 9
⊢ ( bday  “ ({ 0s } ∪ {( 1s
/su (2s↑s𝑛))})) = (( bday 
“ { 0s }) ∪ ( bday  “
{( 1s /su (2s↑s𝑛))})) | 
| 64 | 62, 63 | eqtr4di 2795 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0s
→ (suc ∅ ∪ {( bday ‘(
1s /su (2s↑s𝑛)))}) = (
bday  “ ({ 0s } ∪ {( 1s
/su (2s↑s𝑛))}))) | 
| 65 |  | 0ss 4400 | . . . . . . . . . 10
⊢ ∅
⊆ ( bday ‘( 1s
/su (2s↑s𝑛))) | 
| 66 |  | ord0 6437 | . . . . . . . . . . 11
⊢ Ord
∅ | 
| 67 |  | bdayelon 27821 | . . . . . . . . . . . 12
⊢ ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ On | 
| 68 | 67 | onordi 6495 | . . . . . . . . . . 11
⊢ Ord
( bday ‘( 1s /su
(2s↑s𝑛))) | 
| 69 |  | ordsucsssuc 7843 | . . . . . . . . . . 11
⊢ ((Ord
∅ ∧ Ord ( bday ‘( 1s
/su (2s↑s𝑛)))) → (∅ ⊆ ( bday ‘( 1s /su
(2s↑s𝑛))) ↔ suc ∅ ⊆ suc ( bday ‘( 1s /su
(2s↑s𝑛))))) | 
| 70 | 66, 68, 69 | mp2an 692 | . . . . . . . . . 10
⊢ (∅
⊆ ( bday ‘( 1s
/su (2s↑s𝑛))) ↔ suc ∅ ⊆ suc ( bday ‘( 1s /su
(2s↑s𝑛)))) | 
| 71 | 65, 70 | mpbi 230 | . . . . . . . . 9
⊢ suc
∅ ⊆ suc ( bday ‘( 1s
/su (2s↑s𝑛))) | 
| 72 |  | fvex 6919 | . . . . . . . . . . 11
⊢ ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ V | 
| 73 | 72 | sucid 6466 | . . . . . . . . . 10
⊢ ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ suc ( bday
‘( 1s /su
(2s↑s𝑛))) | 
| 74 |  | snssi 4808 | . . . . . . . . . 10
⊢ (( bday ‘( 1s /su
(2s↑s𝑛))) ∈ suc ( bday
‘( 1s /su
(2s↑s𝑛))) → {( bday
‘( 1s /su
(2s↑s𝑛)))} ⊆ suc ( bday
‘( 1s /su
(2s↑s𝑛)))) | 
| 75 | 73, 74 | ax-mp 5 | . . . . . . . . 9
⊢ {( bday ‘( 1s /su
(2s↑s𝑛)))} ⊆ suc ( bday
‘( 1s /su
(2s↑s𝑛))) | 
| 76 | 71, 75 | unssi 4191 | . . . . . . . 8
⊢ (suc
∅ ∪ {( bday ‘( 1s
/su (2s↑s𝑛)))}) ⊆ suc (
bday ‘( 1s /su
(2s↑s𝑛))) | 
| 77 | 64, 76 | eqsstrrdi 4029 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ ( bday  “ ({ 0s } ∪ {(
1s /su (2s↑s𝑛))})) ⊆ suc ( bday ‘( 1s /su
(2s↑s𝑛)))) | 
| 78 | 67 | onsuci 7859 | . . . . . . . 8
⊢ suc
( bday ‘( 1s /su
(2s↑s𝑛))) ∈ On | 
| 79 |  | scutbdaybnd 27860 | . . . . . . . 8
⊢ (({
0s } <<s {( 1s /su
(2s↑s𝑛))} ∧ suc ( bday
‘( 1s /su
(2s↑s𝑛))) ∈ On ∧ (
bday  “ ({ 0s } ∪ {( 1s
/su (2s↑s𝑛))})) ⊆ suc (
bday ‘( 1s /su
(2s↑s𝑛)))) → ( bday
‘({ 0s } |s {( 1s /su
(2s↑s𝑛))})) ⊆ suc (
bday ‘( 1s /su
(2s↑s𝑛)))) | 
| 80 | 78, 79 | mp3an2 1451 | . . . . . . 7
⊢ (({
0s } <<s {( 1s /su
(2s↑s𝑛))} ∧ ( bday
 “ ({ 0s } ∪ {( 1s /su
(2s↑s𝑛))})) ⊆ suc (
bday ‘( 1s /su
(2s↑s𝑛)))) → ( bday
‘({ 0s } |s {( 1s /su
(2s↑s𝑛))})) ⊆ suc (
bday ‘( 1s /su
(2s↑s𝑛)))) | 
| 81 | 50, 77, 80 | syl2anc 584 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘({ 0s } |s {(
1s /su (2s↑s𝑛))})) ⊆ suc ( bday ‘( 1s /su
(2s↑s𝑛)))) | 
| 82 | 29, 81 | eqsstrd 4018 | . . . . 5
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘( 1s
/su (2s↑s(𝑛 +s 1s )))) ⊆ suc
( bday ‘( 1s /su
(2s↑s𝑛)))) | 
| 83 |  | bdayelon 27821 | . . . . . 6
⊢ ( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈
On | 
| 84 |  | onsssuc 6474 | . . . . . 6
⊢ ((( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈ On
∧ suc ( bday ‘( 1s
/su (2s↑s𝑛))) ∈ On) → (( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ⊆ suc
( bday ‘( 1s /su
(2s↑s𝑛))) ↔ ( bday
‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈ suc
suc ( bday ‘( 1s
/su (2s↑s𝑛))))) | 
| 85 | 83, 78, 84 | mp2an 692 | . . . . 5
⊢ (( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ⊆ suc
( bday ‘( 1s /su
(2s↑s𝑛))) ↔ ( bday
‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈ suc
suc ( bday ‘( 1s
/su (2s↑s𝑛)))) | 
| 86 | 82, 85 | sylib 218 | . . . 4
⊢ (𝑛 ∈ ℕ0s
→ ( bday ‘( 1s
/su (2s↑s(𝑛 +s 1s )))) ∈ suc
suc ( bday ‘( 1s
/su (2s↑s𝑛)))) | 
| 87 |  | peano2 7912 | . . . . 5
⊢ (( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω → suc ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω) | 
| 88 |  | peano2 7912 | . . . . 5
⊢ (suc
( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω → suc suc ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω) | 
| 89 | 87, 88 | syl 17 | . . . 4
⊢ (( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω → suc suc ( bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω) | 
| 90 |  | elnn 7898 | . . . 4
⊢ ((( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈ suc
suc ( bday ‘( 1s
/su (2s↑s𝑛))) ∧ suc suc (
bday ‘( 1s /su
(2s↑s𝑛))) ∈ ω) → ( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈
ω) | 
| 91 | 86, 89, 90 | syl2an 596 | . . 3
⊢ ((𝑛 ∈ ℕ0s
∧ ( bday ‘( 1s
/su (2s↑s𝑛))) ∈ ω) → ( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈
ω) | 
| 92 | 91 | ex 412 | . 2
⊢ (𝑛 ∈ ℕ0s
→ (( bday ‘( 1s
/su (2s↑s𝑛))) ∈ ω → ( bday ‘( 1s /su
(2s↑s(𝑛 +s 1s )))) ∈
ω)) | 
| 93 | 14, 18, 22, 26, 27, 92 | n0sind 28337 | 1
⊢ (𝑁 ∈ ℕ0s
→ ( bday ‘( 1s
/su (2s↑s𝑁))) ∈ ω) |