Step | Hyp | Ref
| Expression |
1 | | df-1s 27186 |
. . 3
⊢
1s = ({ 0s } |s ∅) |
2 | 1 | fveq2i 6846 |
. 2
⊢ ( bday ‘ 1s ) = (
bday ‘({ 0s } |s ∅)) |
3 | | 0sno 27187 |
. . . . . . 7
⊢
0s ∈ No |
4 | | snelpwi 5401 |
. . . . . . 7
⊢ (
0s ∈ No → { 0s }
∈ 𝒫 No ) |
5 | 3, 4 | ax-mp 5 |
. . . . . 6
⊢ {
0s } ∈ 𝒫 No
|
6 | | nulssgt 27159 |
. . . . . 6
⊢ ({
0s } ∈ 𝒫 No → {
0s } <<s ∅) |
7 | 5, 6 | ax-mp 5 |
. . . . 5
⊢ {
0s } <<s ∅ |
8 | | scutbdaybnd2 27177 |
. . . . 5
⊢ ({
0s } <<s ∅ → ( bday
‘({ 0s } |s ∅)) ⊆ suc ∪ ( bday “ ({
0s } ∪ ∅))) |
9 | 7, 8 | ax-mp 5 |
. . . 4
⊢ ( bday ‘({ 0s } |s ∅)) ⊆ suc
∪ ( bday “ ({
0s } ∪ ∅)) |
10 | | un0 4351 |
. . . . . . . . . 10
⊢ ({
0s } ∪ ∅) = { 0s } |
11 | 10 | imaeq2i 6012 |
. . . . . . . . 9
⊢ ( bday “ ({ 0s } ∪ ∅)) =
( bday “ { 0s
}) |
12 | | bdayfn 27135 |
. . . . . . . . . 10
⊢ bday Fn No
|
13 | | fnsnfv 6921 |
. . . . . . . . . 10
⊢ (( bday Fn No ∧
0s ∈ No ) → {( bday ‘ 0s )} = (
bday “ { 0s })) |
14 | 12, 3, 13 | mp2an 691 |
. . . . . . . . 9
⊢ {( bday ‘ 0s )} = (
bday “ { 0s }) |
15 | | bday0s 27189 |
. . . . . . . . . 10
⊢ ( bday ‘ 0s ) = ∅ |
16 | 15 | sneqi 4598 |
. . . . . . . . 9
⊢ {( bday ‘ 0s )} =
{∅} |
17 | 11, 14, 16 | 3eqtr2i 2767 |
. . . . . . . 8
⊢ ( bday “ ({ 0s } ∪ ∅)) =
{∅} |
18 | 17 | unieqi 4879 |
. . . . . . 7
⊢ ∪ ( bday “ ({
0s } ∪ ∅)) = ∪
{∅} |
19 | | 0ex 5265 |
. . . . . . . 8
⊢ ∅
∈ V |
20 | 19 | unisn 4888 |
. . . . . . 7
⊢ ∪ {∅} = ∅ |
21 | 18, 20 | eqtri 2761 |
. . . . . 6
⊢ ∪ ( bday “ ({
0s } ∪ ∅)) = ∅ |
22 | | suceq 6384 |
. . . . . 6
⊢ (∪ ( bday “ ({
0s } ∪ ∅)) = ∅ → suc ∪ ( bday “ ({
0s } ∪ ∅)) = suc ∅) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
⊢ suc ∪ ( bday “ ({
0s } ∪ ∅)) = suc ∅ |
24 | | df-1o 8413 |
. . . . 5
⊢
1o = suc ∅ |
25 | 23, 24 | eqtr4i 2764 |
. . . 4
⊢ suc ∪ ( bday “ ({
0s } ∪ ∅)) = 1o |
26 | 9, 25 | sseqtri 3981 |
. . 3
⊢ ( bday ‘({ 0s } |s ∅)) ⊆
1o |
27 | | ssrab2 4038 |
. . . . . 6
⊢ {𝑥 ∈
No ∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} ⊆ No |
28 | | fnssintima 7308 |
. . . . . 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 691 |
. . . . 5
⊢
(1o ⊆ ∩ ( bday “ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}) ↔ ∀𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}1o ⊆
( bday ‘𝑦)) |
30 | | sneq 4597 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
31 | 30 | breq2d 5118 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({ 0s } <<s {𝑥} ↔ { 0s }
<<s {𝑦})) |
32 | 30 | breq1d 5116 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ({𝑥} <<s ∅ ↔ {𝑦} <<s
∅)) |
33 | 31, 32 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅) ↔ ({ 0s
} <<s {𝑦} ∧
{𝑦} <<s
∅))) |
34 | 33 | elrab 3646 |
. . . . . 6
⊢ (𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} ↔ (𝑦 ∈
No ∧ ({ 0s } <<s {𝑦} ∧ {𝑦} <<s ∅))) |
35 | | sltirr 27110 |
. . . . . . . . . . . . 13
⊢ (
0s ∈ No → ¬
0s <s 0s ) |
36 | 3, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬
0s <s 0s |
37 | | breq2 5110 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0s → (
0s <s 𝑦
↔ 0s <s 0s )) |
38 | 36, 37 | mtbiri 327 |
. . . . . . . . . . 11
⊢ (𝑦 = 0s → ¬
0s <s 𝑦) |
39 | 38 | necon2ai 2970 |
. . . . . . . . . 10
⊢ (
0s <s 𝑦
→ 𝑦 ≠ 0s
) |
40 | | bday0b 27191 |
. . . . . . . . . . 11
⊢ (𝑦 ∈
No → (( bday ‘𝑦) = ∅ ↔ 𝑦 = 0s
)) |
41 | 40 | necon3bid 2985 |
. . . . . . . . . 10
⊢ (𝑦 ∈
No → (( bday ‘𝑦) ≠ ∅ ↔ 𝑦 ≠ 0s
)) |
42 | 39, 41 | syl5ibr 246 |
. . . . . . . . 9
⊢ (𝑦 ∈
No → ( 0s <s 𝑦 → ( bday
‘𝑦) ≠
∅)) |
43 | | bdayelon 27138 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑦) ∈ On |
44 | 43 | onordi 6429 |
. . . . . . . . . 10
⊢ Ord
( bday ‘𝑦) |
45 | | ordge1n0 8441 |
. . . . . . . . . 10
⊢ (Ord
( bday ‘𝑦) → (1o ⊆ ( bday ‘𝑦) ↔ ( bday
‘𝑦) ≠
∅)) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . . 9
⊢
(1o ⊆ ( bday ‘𝑦) ↔ (
bday ‘𝑦) ≠
∅) |
47 | 42, 46 | syl6ibr 252 |
. . . . . . . 8
⊢ (𝑦 ∈
No → ( 0s <s 𝑦 → 1o ⊆ ( bday ‘𝑦))) |
48 | | ssltsep 27152 |
. . . . . . . . 9
⊢ ({
0s } <<s {𝑦} → ∀𝑥 ∈ { 0s }∀𝑧 ∈ {𝑦}𝑥 <s 𝑧) |
49 | | vex 3448 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
50 | | breq2 5110 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑥 <s 𝑧 ↔ 𝑥 <s 𝑦)) |
51 | 49, 50 | ralsn 4643 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
{𝑦}𝑥 <s 𝑧 ↔ 𝑥 <s 𝑦) |
52 | 51 | ralbii 3093 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ {
0s }∀𝑧
∈ {𝑦}𝑥 <s 𝑧 ↔ ∀𝑥 ∈ { 0s }𝑥 <s 𝑦) |
53 | 3 | elexi 3463 |
. . . . . . . . . . 11
⊢
0s ∈ V |
54 | | breq1 5109 |
. . . . . . . . . . 11
⊢ (𝑥 = 0s → (𝑥 <s 𝑦 ↔ 0s <s 𝑦)) |
55 | 53, 54 | ralsn 4643 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ {
0s }𝑥 <s
𝑦 ↔ 0s
<s 𝑦) |
56 | 52, 55 | bitri 275 |
. . . . . . . . 9
⊢
(∀𝑥 ∈ {
0s }∀𝑧
∈ {𝑦}𝑥 <s 𝑧 ↔ 0s <s 𝑦) |
57 | 48, 56 | sylib 217 |
. . . . . . . 8
⊢ ({
0s } <<s {𝑦} → 0s <s 𝑦) |
58 | 47, 57 | impel 507 |
. . . . . . 7
⊢ ((𝑦 ∈
No ∧ { 0s } <<s {𝑦}) → 1o ⊆ ( bday ‘𝑦)) |
59 | 58 | adantrr 716 |
. . . . . 6
⊢ ((𝑦 ∈
No ∧ ({ 0s } <<s {𝑦} ∧ {𝑦} <<s ∅)) → 1o
⊆ ( bday ‘𝑦)) |
60 | 34, 59 | sylbi 216 |
. . . . 5
⊢ (𝑦 ∈ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)} → 1o
⊆ ( bday ‘𝑦)) |
61 | 29, 60 | mprgbir 3068 |
. . . 4
⊢
1o ⊆ ∩ ( bday “ {𝑥 ∈ No
∣ ({ 0s } <<s {𝑥} ∧ {𝑥} <<s ∅)}) |
62 | | scutbday 27165 |
. . . . 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 3982 |
. . 3
⊢
1o ⊆ ( bday ‘({
0s } |s ∅)) |
65 | 26, 64 | eqssi 3961 |
. 2
⊢ ( bday ‘({ 0s } |s ∅)) =
1o |
66 | 2, 65 | eqtri 2761 |
1
⊢ ( bday ‘ 1s ) =
1o |