Step | Hyp | Ref
| Expression |
1 | | df-1s 33662 |
. . 3
⊢ 1s = ({
0s } |s ∅) |
2 | 1 | fveq2i 6677 |
. 2
⊢ ( bday ‘ 1s ) = ( bday
‘({ 0s } |s ∅)) |
3 | | 0sno 33663 |
. . . . . . 7
⊢ 0s
∈ No |
4 | | snelpwi 5303 |
. . . . . . 7
⊢ ( 0s
∈ No → { 0s } ∈ 𝒫 No ) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ { 0s }
∈ 𝒫 No |
6 | | nulssgt 33635 |
. . . . . 6
⊢ ({ 0s }
∈ 𝒫 No → { 0s } <<s
∅) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ { 0s }
<<s ∅ |
8 | | scutbdaybnd2 33653 |
. . . . 5
⊢ ({ 0s }
<<s ∅ → ( bday ‘({ 0s } |s
∅)) ⊆ suc ∪ ( bday
“ ({ 0s } ∪ ∅))) |
9 | 7, 8 | ax-mp 5 |
. . . 4
⊢ ( bday ‘({ 0s } |s ∅)) ⊆ suc ∪ ( bday “ ({ 0s }
∪ ∅)) |
10 | | un0 4279 |
. . . . . . . . . 10
⊢ ({ 0s }
∪ ∅) = { 0s } |
11 | 10 | imaeq2i 5901 |
. . . . . . . . 9
⊢ ( bday “ ({ 0s } ∪ ∅)) = ( bday “ { 0s }) |
12 | | bdayfn 33611 |
. . . . . . . . . 10
⊢ bday Fn No
|
13 | | fnsnfv 6747 |
. . . . . . . . . 10
⊢ (( bday Fn No ∧ 0s
∈ No ) → {( bday
‘ 0s )} = ( bday “ { 0s
})) |
14 | 12, 3, 13 | mp2an 692 |
. . . . . . . . 9
⊢ {( bday ‘ 0s )} = ( bday
“ { 0s }) |
15 | | bday0s 33665 |
. . . . . . . . . 10
⊢ ( bday ‘ 0s ) = ∅ |
16 | 15 | sneqi 4527 |
. . . . . . . . 9
⊢ {( bday ‘ 0s )} = {∅} |
17 | 11, 14, 16 | 3eqtr2i 2767 |
. . . . . . . 8
⊢ ( bday “ ({ 0s } ∪ ∅)) =
{∅} |
18 | 17 | unieqi 4809 |
. . . . . . 7
⊢ ∪ ( bday “ ({ 0s }
∪ ∅)) = ∪ {∅} |
19 | | 0ex 5175 |
. . . . . . . 8
⊢ ∅
∈ V |
20 | 19 | unisn 4818 |
. . . . . . 7
⊢ ∪ {∅} = ∅ |
21 | 18, 20 | eqtri 2761 |
. . . . . 6
⊢ ∪ ( bday “ ({ 0s }
∪ ∅)) = ∅ |
22 | | suceq 6237 |
. . . . . 6
⊢ (∪ ( bday “ ({ 0s }
∪ ∅)) = ∅ → suc ∪ ( bday “ ({ 0s } ∪ ∅)) = suc
∅) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
⊢ suc ∪ ( bday “ ({ 0s }
∪ ∅)) = suc ∅ |
24 | | df-1o 8131 |
. . . . 5
⊢
1o = suc ∅ |
25 | 23, 24 | eqtr4i 2764 |
. . . 4
⊢ suc ∪ ( bday “ ({ 0s }
∪ ∅)) = 1o |
26 | 9, 25 | sseqtri 3913 |
. . 3
⊢ ( bday ‘({ 0s } |s ∅)) ⊆
1o |
27 | | ssrab2 3969 |
. . . . . 6
⊢ {𝑥 ∈
No ∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} ⊆ No |
28 | | fnssintima 33249 |
. . . . . 6
⊢ (( bday Fn No ∧ {𝑥 ∈
No ∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} ⊆ No ) → (1o ⊆ ∩ ( bday “ {𝑥 ∈
No ∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}) ↔ ∀𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}1o ⊆
( bday ‘𝑦))) |
29 | 12, 27, 28 | mp2an 692 |
. . . . 5
⊢
(1o ⊆ ∩ ( bday “ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}) ↔ ∀𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}1o ⊆
( bday ‘𝑦)) |
30 | | sneq 4526 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
31 | 30 | breq2d 5042 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({ 0s } <<s {𝑥} ↔ { 0s } <<s {𝑦})) |
32 | 30 | breq1d 5040 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({𝑥} <<s ∅ ↔ {𝑦} <<s
∅)) |
33 | 31, 32 | anbi12d 634 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅) ↔ ({ 0s } <<s
{𝑦} ∧ {𝑦} <<s
∅))) |
34 | 33 | elrab 3588 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} ↔ (𝑦 ∈
No ∧ ({ 0s } <<s {𝑦} ∧ {𝑦} <<s ∅))) |
35 | | sltirr 33592 |
. . . . . . . . . . . . 13
⊢ ( 0s
∈ No → ¬ 0s <s 0s
) |
36 | 3, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬ 0s
<s 0s |
37 | | breq2 5034 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0s → ( 0s <s 𝑦 ↔ 0s <s 0s
)) |
38 | 36, 37 | mtbiri 330 |
. . . . . . . . . . 11
⊢ (𝑦 = 0s → ¬ 0s <s
𝑦) |
39 | 38 | necon2ai 2963 |
. . . . . . . . . 10
⊢ ( 0s
<s 𝑦 → 𝑦 ≠ 0s ) |
40 | | bday0b 33667 |
. . . . . . . . . . 11
⊢ (𝑦 ∈
No → (( bday ‘𝑦) = ∅ ↔ 𝑦 = 0s )) |
41 | 40 | necon3bid 2978 |
. . . . . . . . . 10
⊢ (𝑦 ∈
No → (( bday ‘𝑦) ≠ ∅ ↔ 𝑦 ≠ 0s )) |
42 | 39, 41 | syl5ibr 249 |
. . . . . . . . 9
⊢ (𝑦 ∈
No → ( 0s <s 𝑦 → ( bday
‘𝑦) ≠
∅)) |
43 | | bdayelon 33614 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑦) ∈ On |
44 | 43 | onordi 6277 |
. . . . . . . . . 10
⊢ Ord
( bday ‘𝑦) |
45 | | ordge1n0 8154 |
. . . . . . . . . 10
⊢ (Ord
( bday ‘𝑦) → (1o ⊆ ( bday ‘𝑦) ↔ ( bday
‘𝑦) ≠
∅)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . 9
⊢
(1o ⊆ ( bday ‘𝑦) ↔ (
bday ‘𝑦) ≠
∅) |
47 | 42, 46 | syl6ibr 255 |
. . . . . . . 8
⊢ (𝑦 ∈
No → ( 0s <s 𝑦 → 1o ⊆ ( bday ‘𝑦))) |
48 | | ssltsep 33628 |
. . . . . . . . 9
⊢ ({ 0s }
<<s {𝑦} →
∀𝑥 ∈ { 0s
}∀𝑧 ∈ {𝑦}𝑥 <s 𝑧) |
49 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
50 | | breq2 5034 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑥 <s 𝑧 ↔ 𝑥 <s 𝑦)) |
51 | 49, 50 | ralsn 4572 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
{𝑦}𝑥 <s 𝑧 ↔ 𝑥 <s 𝑦) |
52 | 51 | ralbii 3080 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ {
0s }∀𝑧 ∈ {𝑦}𝑥 <s 𝑧 ↔ ∀𝑥 ∈ { 0s }𝑥 <s 𝑦) |
53 | 3 | elexi 3417 |
. . . . . . . . . . 11
⊢ 0s
∈ V |
54 | | breq1 5033 |
. . . . . . . . . . 11
⊢ (𝑥 = 0s → (𝑥 <s 𝑦 ↔ 0s <s 𝑦)) |
55 | 53, 54 | ralsn 4572 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ {
0s }𝑥 <s 𝑦 ↔ 0s <s 𝑦) |
56 | 52, 55 | bitri 278 |
. . . . . . . . 9
⊢
(∀𝑥 ∈ {
0s }∀𝑧 ∈ {𝑦}𝑥 <s 𝑧 ↔ 0s <s 𝑦) |
57 | 48, 56 | sylib 221 |
. . . . . . . 8
⊢ ({ 0s }
<<s {𝑦} → 0s
<s 𝑦) |
58 | 47, 57 | impel 509 |
. . . . . . 7
⊢ ((𝑦 ∈
No ∧ { 0s } <<s {𝑦}) → 1o ⊆ ( bday ‘𝑦)) |
59 | 58 | adantrr 717 |
. . . . . 6
⊢ ((𝑦 ∈
No ∧ ({ 0s } <<s {𝑦} ∧ {𝑦} <<s ∅)) → 1o
⊆ ( bday ‘𝑦)) |
60 | 34, 59 | sylbi 220 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} → 1o
⊆ ( bday ‘𝑦)) |
61 | 29, 60 | mprgbir 3068 |
. . . 4
⊢
1o ⊆ ∩ ( bday “ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}) |
62 | | scutbday 33641 |
. . . . 5
⊢ ({ 0s }
<<s ∅ → ( bday ‘({ 0s } |s
∅)) = ∩ ( bday
“ {𝑥 ∈ No ∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)})) |
63 | 7, 62 | ax-mp 5 |
. . . 4
⊢ ( bday ‘({ 0s } |s ∅)) = ∩ ( bday “ {𝑥 ∈
No ∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}) |
64 | 61, 63 | sseqtrri 3914 |
. . 3
⊢
1o ⊆ ( bday ‘({ 0s }
|s ∅)) |
65 | 26, 64 | eqssi 3893 |
. 2
⊢ ( bday ‘({ 0s } |s ∅)) =
1o |
66 | 2, 65 | eqtri 2761 |
1
⊢ ( bday ‘ 1s ) = 1o |