| Step | Hyp | Ref
| Expression |
| 1 | | snex 5436 |
. . . . . . . 8
⊢ {
0s } ∈ V |
| 2 | 1 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ { 0s } ∈ V) |
| 3 | | snex 5436 |
. . . . . . . 8
⊢ {
1s } ∈ V |
| 4 | 3 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ { 1s } ∈ V) |
| 5 | | 0sno 27871 |
. . . . . . . . 9
⊢
0s ∈ No |
| 6 | 5 | a1i 11 |
. . . . . . . 8
⊢ (⊤
→ 0s ∈ No ) |
| 7 | 6 | snssd 4809 |
. . . . . . 7
⊢ (⊤
→ { 0s } ⊆ No
) |
| 8 | | 1sno 27872 |
. . . . . . . 8
⊢
1s ∈ No |
| 9 | | snssi 4808 |
. . . . . . . 8
⊢ (
1s ∈ No → { 1s }
⊆ No ) |
| 10 | 8, 9 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ { 1s } ⊆ No
) |
| 11 | | velsn 4642 |
. . . . . . . . 9
⊢ (𝑥 ∈ { 0s } ↔
𝑥 = 0s
) |
| 12 | | velsn 4642 |
. . . . . . . . 9
⊢ (𝑦 ∈ { 1s } ↔
𝑦 = 1s
) |
| 13 | | 0slt1s 27874 |
. . . . . . . . . 10
⊢
0s <s 1s |
| 14 | | breq12 5148 |
. . . . . . . . . 10
⊢ ((𝑥 = 0s ∧ 𝑦 = 1s ) → (𝑥 <s 𝑦 ↔ 0s <s 1s
)) |
| 15 | 13, 14 | mpbiri 258 |
. . . . . . . . 9
⊢ ((𝑥 = 0s ∧ 𝑦 = 1s ) → 𝑥 <s 𝑦) |
| 16 | 11, 12, 15 | syl2anb 598 |
. . . . . . . 8
⊢ ((𝑥 ∈ { 0s } ∧
𝑦 ∈ { 1s })
→ 𝑥 <s 𝑦) |
| 17 | 16 | 3adant1 1131 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ { 0s } ∧ 𝑦 ∈ { 1s }) → 𝑥 <s 𝑦) |
| 18 | 2, 4, 7, 10, 17 | ssltd 27836 |
. . . . . 6
⊢ (⊤
→ { 0s } <<s { 1s }) |
| 19 | 18 | scutcld 27848 |
. . . . 5
⊢ (⊤
→ ({ 0s } |s { 1s }) ∈
No ) |
| 20 | 19 | mptru 1547 |
. . . 4
⊢ ({
0s } |s { 1s }) ∈ No
|
| 21 | | no2times 28401 |
. . . 4
⊢ (({
0s } |s { 1s }) ∈ No
→ (2s ·s ({ 0s } |s {
1s })) = (({ 0s } |s { 1s }) +s ({
0s } |s { 1s }))) |
| 22 | 20, 21 | ax-mp 5 |
. . 3
⊢
(2s ·s ({ 0s } |s {
1s })) = (({ 0s } |s { 1s }) +s ({
0s } |s { 1s })) |
| 23 | | eqidd 2738 |
. . . . . 6
⊢ (⊤
→ ({ 0s } |s { 1s }) = ({ 0s } |s {
1s })) |
| 24 | 18, 18, 23, 23 | addsunif 28035 |
. . . . 5
⊢ (⊤
→ (({ 0s } |s { 1s }) +s ({ 0s
} |s { 1s })) = (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
0s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}))) |
| 25 | 24 | mptru 1547 |
. . . 4
⊢ (({
0s } |s { 1s }) +s ({ 0s } |s {
1s })) = (({𝑥
∣ ∃𝑦 ∈ {
0s }𝑥 = (𝑦 +s ({ 0s
} |s { 1s }))} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s { 1s })
+s 𝑦)}) |s
({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)})) |
| 26 | 5 | elexi 3503 |
. . . . . . . . . . 11
⊢
0s ∈ V |
| 27 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0s → (𝑦 +s ({ 0s
} |s { 1s })) = ( 0s +s ({ 0s } |s
{ 1s }))) |
| 28 | | addslid 28001 |
. . . . . . . . . . . . . 14
⊢ (({
0s } |s { 1s }) ∈ No
→ ( 0s +s ({ 0s } |s { 1s }))
= ({ 0s } |s { 1s })) |
| 29 | 20, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (
0s +s ({ 0s } |s { 1s })) = ({
0s } |s { 1s }) |
| 30 | 27, 29 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0s → (𝑦 +s ({ 0s
} |s { 1s })) = ({ 0s } |s { 1s
})) |
| 31 | 30 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s ({ 0s } |s {
1s })) ↔ 𝑥
= ({ 0s } |s { 1s }))) |
| 32 | 26, 31 | rexsn 4682 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ {
0s }𝑥 = (𝑦 +s ({ 0s
} |s { 1s })) ↔ 𝑥 = ({ 0s } |s { 1s
})) |
| 33 | 32 | abbii 2809 |
. . . . . . . . 9
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} = {𝑥
∣ 𝑥 = ({
0s } |s { 1s })} |
| 34 | | df-sn 4627 |
. . . . . . . . 9
⊢ {({
0s } |s { 1s })} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s
})} |
| 35 | 33, 34 | eqtr4i 2768 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} = {({ 0s } |s { 1s
})} |
| 36 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 0s → (({
0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s })
+s 0s )) |
| 37 | | addsrid 27997 |
. . . . . . . . . . . . . 14
⊢ (({
0s } |s { 1s }) ∈ No
→ (({ 0s } |s { 1s }) +s 0s )
= ({ 0s } |s { 1s })) |
| 38 | 20, 37 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (({
0s } |s { 1s }) +s 0s ) = ({
0s } |s { 1s }) |
| 39 | 36, 38 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑦 = 0s → (({
0s } |s { 1s }) +s 𝑦) = ({ 0s } |s { 1s
})) |
| 40 | 39 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = 0s → (𝑥 = (({ 0s } |s {
1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s
}))) |
| 41 | 26, 40 | rexsn 4682 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ {
0s }𝑥 = (({
0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = ({ 0s } |s { 1s
})) |
| 42 | 41 | abbii 2809 |
. . . . . . . . 9
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s {
1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = ({ 0s } |s { 1s
})} |
| 43 | 42, 34 | eqtr4i 2768 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (({ 0s } |s {
1s }) +s 𝑦)} = {({ 0s } |s { 1s
})} |
| 44 | 35, 43 | uneq12i 4166 |
. . . . . . 7
⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
0s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) = ({({ 0s } |s { 1s
})} ∪ {({ 0s } |s { 1s })}) |
| 45 | | unidm 4157 |
. . . . . . 7
⊢ ({({
0s } |s { 1s })} ∪ {({ 0s } |s {
1s })}) = {({ 0s } |s { 1s
})} |
| 46 | 44, 45 | eqtri 2765 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
0s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) = {({ 0s } |s { 1s
})} |
| 47 | 8 | elexi 3503 |
. . . . . . . . . . 11
⊢
1s ∈ V |
| 48 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 1s → (𝑦 +s ({ 0s
} |s { 1s })) = ( 1s +s ({ 0s } |s
{ 1s }))) |
| 49 | | addscom 27999 |
. . . . . . . . . . . . . 14
⊢ ((
1s ∈ No ∧ ({ 0s }
|s { 1s }) ∈ No ) → (
1s +s ({ 0s } |s { 1s })) = (({
0s } |s { 1s }) +s 1s
)) |
| 50 | 8, 20, 49 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (
1s +s ({ 0s } |s { 1s })) = (({
0s } |s { 1s }) +s 1s
) |
| 51 | 48, 50 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1s → (𝑦 +s ({ 0s
} |s { 1s })) = (({ 0s } |s { 1s })
+s 1s )) |
| 52 | 51 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = 1s → (𝑥 = (𝑦 +s ({ 0s } |s {
1s })) ↔ 𝑥
= (({ 0s } |s { 1s }) +s 1s
))) |
| 53 | 47, 52 | rexsn 4682 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ {
1s }𝑥 = (𝑦 +s ({ 0s
} |s { 1s })) ↔ 𝑥 = (({ 0s } |s { 1s })
+s 1s )) |
| 54 | 53 | abbii 2809 |
. . . . . . . . 9
⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} = {𝑥
∣ 𝑥 = (({
0s } |s { 1s }) +s 1s
)} |
| 55 | | df-sn 4627 |
. . . . . . . . 9
⊢ {(({
0s } |s { 1s }) +s 1s )} = {𝑥 ∣ 𝑥 = (({ 0s } |s { 1s })
+s 1s )} |
| 56 | 54, 55 | eqtr4i 2768 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} = {(({ 0s } |s { 1s }) +s
1s )} |
| 57 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1s → (({
0s } |s { 1s }) +s 𝑦) = (({ 0s } |s { 1s })
+s 1s )) |
| 58 | 57 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = 1s → (𝑥 = (({ 0s } |s {
1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s })
+s 1s ))) |
| 59 | 47, 58 | rexsn 4682 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦) ↔ 𝑥 = (({ 0s } |s { 1s })
+s 1s )) |
| 60 | 59 | abbii 2809 |
. . . . . . . . 9
⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s {
1s }) +s 𝑦)} = {𝑥 ∣ 𝑥 = (({ 0s } |s { 1s })
+s 1s )} |
| 61 | 60, 55 | eqtr4i 2768 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (({ 0s } |s {
1s }) +s 𝑦)} = {(({ 0s } |s { 1s
}) +s 1s )} |
| 62 | 56, 61 | uneq12i 4166 |
. . . . . . 7
⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) = ({(({ 0s } |s {
1s }) +s 1s )} ∪ {(({ 0s } |s {
1s }) +s 1s )}) |
| 63 | | unidm 4157 |
. . . . . . 7
⊢ ({(({
0s } |s { 1s }) +s 1s )} ∪ {(({
0s } |s { 1s }) +s 1s )}) = {(({
0s } |s { 1s }) +s 1s
)} |
| 64 | 62, 63 | eqtri 2765 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) = {(({ 0s } |s { 1s
}) +s 1s )} |
| 65 | 46, 64 | oveq12i 7443 |
. . . . 5
⊢ (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
0s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)})) = ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}) |
| 66 | | ral0 4513 |
. . . . . . 7
⊢
∀𝑥 ∈
∅ ({({ 0s } |s { 1s })} |s {(({ 0s } |s
{ 1s }) +s 1s )}) <s 𝑥 |
| 67 | | slerflex 27808 |
. . . . . . . . . . . 12
⊢ (
1s ∈ No → 1s
≤s 1s ) |
| 68 | 8, 67 | ax-mp 5 |
. . . . . . . . . . 11
⊢
1s ≤s 1s |
| 69 | | breq1 5146 |
. . . . . . . . . . . 12
⊢ (𝑦 = 1s → (𝑦 ≤s 1s ↔
1s ≤s 1s )) |
| 70 | 47, 69 | rexsn 4682 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈ {
1s }𝑦 ≤s
1s ↔ 1s ≤s 1s ) |
| 71 | 68, 70 | mpbir 231 |
. . . . . . . . . 10
⊢
∃𝑦 ∈ {
1s }𝑦 ≤s
1s |
| 72 | 71 | olci 867 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ {
0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s ) |
| 73 | 18 | mptru 1547 |
. . . . . . . . . 10
⊢ {
0s } <<s { 1s } |
| 74 | | snelpwi 5448 |
. . . . . . . . . . . 12
⊢ (
0s ∈ No → { 0s }
∈ 𝒫 No ) |
| 75 | 5, 74 | ax-mp 5 |
. . . . . . . . . . 11
⊢ {
0s } ∈ 𝒫 No
|
| 76 | | nulssgt 27843 |
. . . . . . . . . . 11
⊢ ({
0s } ∈ 𝒫 No → {
0s } <<s ∅) |
| 77 | 75, 76 | ax-mp 5 |
. . . . . . . . . 10
⊢ {
0s } <<s ∅ |
| 78 | | eqid 2737 |
. . . . . . . . . 10
⊢ ({
0s } |s { 1s }) = ({ 0s } |s { 1s
}) |
| 79 | | df-1s 27870 |
. . . . . . . . . 10
⊢
1s = ({ 0s } |s ∅) |
| 80 | | sltrec 27865 |
. . . . . . . . . 10
⊢ ((({
0s } <<s { 1s } ∧ { 0s } <<s
∅) ∧ (({ 0s } |s { 1s }) = ({ 0s }
|s { 1s }) ∧ 1s = ({ 0s } |s ∅)))
→ (({ 0s } |s { 1s }) <s 1s ↔
(∃𝑥 ∈ {
0s } ({ 0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s ))) |
| 81 | 73, 77, 78, 79, 80 | mp4an 693 |
. . . . . . . . 9
⊢ (({
0s } |s { 1s }) <s 1s ↔ (∃𝑥 ∈ { 0s } ({
0s } |s { 1s }) ≤s 𝑥 ∨ ∃𝑦 ∈ { 1s }𝑦 ≤s 1s )) |
| 82 | 72, 81 | mpbir 231 |
. . . . . . . 8
⊢ ({
0s } |s { 1s }) <s 1s |
| 83 | | ovex 7464 |
. . . . . . . . 9
⊢ ({
0s } |s { 1s }) ∈ V |
| 84 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑦 = ({ 0s } |s {
1s }) → (𝑦
<s 1s ↔ ({ 0s } |s { 1s }) <s
1s )) |
| 85 | 83, 84 | ralsn 4681 |
. . . . . . . 8
⊢
(∀𝑦 ∈
{({ 0s } |s { 1s })}𝑦 <s 1s ↔ ({ 0s
} |s { 1s }) <s 1s ) |
| 86 | 82, 85 | mpbir 231 |
. . . . . . 7
⊢
∀𝑦 ∈ {({
0s } |s { 1s })}𝑦 <s 1s |
| 87 | | snex 5436 |
. . . . . . . . . . 11
⊢ {({
0s } |s { 1s })} ∈ V |
| 88 | 87 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ {({ 0s } |s { 1s })} ∈ V) |
| 89 | | snex 5436 |
. . . . . . . . . . 11
⊢ {(({
0s } |s { 1s }) +s 1s )} ∈
V |
| 90 | 89 | a1i 11 |
. . . . . . . . . 10
⊢ (⊤
→ {(({ 0s } |s { 1s }) +s 1s
)} ∈ V) |
| 91 | 19 | snssd 4809 |
. . . . . . . . . 10
⊢ (⊤
→ {({ 0s } |s { 1s })} ⊆ No ) |
| 92 | 8 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 1s ∈ No ) |
| 93 | 19, 92 | addscld 28013 |
. . . . . . . . . . 11
⊢ (⊤
→ (({ 0s } |s { 1s }) +s 1s )
∈ No ) |
| 94 | 93 | snssd 4809 |
. . . . . . . . . 10
⊢ (⊤
→ {(({ 0s } |s { 1s }) +s 1s
)} ⊆ No ) |
| 95 | | velsn 4642 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {({ 0s } |s {
1s })} ↔ 𝑥
= ({ 0s } |s { 1s })) |
| 96 | | velsn 4642 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ {(({ 0s } |s
{ 1s }) +s 1s )} ↔ 𝑦 = (({ 0s } |s { 1s })
+s 1s )) |
| 97 | | sltadd2 28024 |
. . . . . . . . . . . . . . . 16
⊢ ((
0s ∈ No ∧ 1s
∈ No ∧ ({ 0s } |s {
1s }) ∈ No ) → (
0s <s 1s ↔ (({ 0s } |s { 1s
}) +s 0s ) <s (({ 0s } |s { 1s
}) +s 1s ))) |
| 98 | 5, 8, 20, 97 | mp3an 1463 |
. . . . . . . . . . . . . . 15
⊢ (
0s <s 1s ↔ (({ 0s } |s { 1s
}) +s 0s ) <s (({ 0s } |s { 1s
}) +s 1s )) |
| 99 | 13, 98 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢ (({
0s } |s { 1s }) +s 0s ) <s (({
0s } |s { 1s }) +s 1s
) |
| 100 | 38, 99 | eqbrtrri 5166 |
. . . . . . . . . . . . 13
⊢ ({
0s } |s { 1s }) <s (({ 0s } |s {
1s }) +s 1s ) |
| 101 | | breq12 5148 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ({ 0s } |s {
1s }) ∧ 𝑦 =
(({ 0s } |s { 1s }) +s 1s )) →
(𝑥 <s 𝑦 ↔ ({ 0s } |s { 1s
}) <s (({ 0s } |s { 1s }) +s 1s
))) |
| 102 | 100, 101 | mpbiri 258 |
. . . . . . . . . . . 12
⊢ ((𝑥 = ({ 0s } |s {
1s }) ∧ 𝑦 =
(({ 0s } |s { 1s }) +s 1s )) →
𝑥 <s 𝑦) |
| 103 | 95, 96, 102 | syl2anb 598 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ {({ 0s } |s {
1s })} ∧ 𝑦
∈ {(({ 0s } |s { 1s }) +s 1s
)}) → 𝑥 <s 𝑦) |
| 104 | 103 | 3adant1 1131 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ {({ 0s } |s { 1s })} ∧ 𝑦 ∈ {(({ 0s } |s {
1s }) +s 1s )}) → 𝑥 <s 𝑦) |
| 105 | 88, 90, 91, 94, 104 | ssltd 27836 |
. . . . . . . . 9
⊢ (⊤
→ {({ 0s } |s { 1s })} <<s {(({ 0s
} |s { 1s }) +s 1s )}) |
| 106 | 105 | mptru 1547 |
. . . . . . . 8
⊢ {({
0s } |s { 1s })} <<s {(({ 0s } |s {
1s }) +s 1s )} |
| 107 | | eqid 2737 |
. . . . . . . 8
⊢ ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) = ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}) |
| 108 | | slerec 27864 |
. . . . . . . 8
⊢ ((({({
0s } |s { 1s })} <<s {(({ 0s } |s {
1s }) +s 1s )} ∧ { 0s }
<<s ∅) ∧ (({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s )}) = ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ∧ 1s = ({
0s } |s ∅))) → (({({ 0s } |s { 1s
})} |s {(({ 0s } |s { 1s }) +s 1s
)}) ≤s 1s ↔ (∀𝑥 ∈ ∅ ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}) <s 𝑥
∧ ∀𝑦 ∈ {({
0s } |s { 1s })}𝑦 <s 1s ))) |
| 109 | 106, 77, 107, 79, 108 | mp4an 693 |
. . . . . . 7
⊢ (({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ≤s 1s ↔
(∀𝑥 ∈ ∅
({({ 0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) <s 𝑥 ∧ ∀𝑦 ∈ {({ 0s } |s {
1s })}𝑦 <s
1s )) |
| 110 | 66, 86, 109 | mpbir2an 711 |
. . . . . 6
⊢ ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ≤s
1s |
| 111 | | addslid 28001 |
. . . . . . . . . 10
⊢ (
1s ∈ No → ( 0s
+s 1s ) = 1s ) |
| 112 | 8, 111 | ax-mp 5 |
. . . . . . . . 9
⊢ (
0s +s 1s ) = 1s |
| 113 | | slerflex 27808 |
. . . . . . . . . . . . . 14
⊢ (
0s ∈ No → 0s
≤s 0s ) |
| 114 | 5, 113 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
0s ≤s 0s |
| 115 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 0s → (
0s ≤s 𝑥
↔ 0s ≤s 0s )) |
| 116 | 26, 115 | rexsn 4682 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈ {
0s } 0s ≤s 𝑥 ↔ 0s ≤s 0s
) |
| 117 | 114, 116 | mpbir 231 |
. . . . . . . . . . . 12
⊢
∃𝑥 ∈ {
0s } 0s ≤s 𝑥 |
| 118 | 117 | orci 866 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈ {
0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s
})) |
| 119 | | 0elpw 5356 |
. . . . . . . . . . . . 13
⊢ ∅
∈ 𝒫 No |
| 120 | | nulssgt 27843 |
. . . . . . . . . . . . 13
⊢ (∅
∈ 𝒫 No → ∅ <<s
∅) |
| 121 | 119, 120 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ∅
<<s ∅ |
| 122 | | df-0s 27869 |
. . . . . . . . . . . 12
⊢
0s = (∅ |s ∅) |
| 123 | | sltrec 27865 |
. . . . . . . . . . . 12
⊢
(((∅ <<s ∅ ∧ { 0s } <<s {
1s }) ∧ ( 0s = (∅ |s ∅) ∧ ({
0s } |s { 1s }) = ({ 0s } |s { 1s
}))) → ( 0s <s ({ 0s } |s { 1s })
↔ (∃𝑥 ∈ {
0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s
})))) |
| 124 | 121, 73, 122, 78, 123 | mp4an 693 |
. . . . . . . . . . 11
⊢ (
0s <s ({ 0s } |s { 1s }) ↔
(∃𝑥 ∈ {
0s } 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({ 0s } |s { 1s
}))) |
| 125 | 118, 124 | mpbir 231 |
. . . . . . . . . 10
⊢
0s <s ({ 0s } |s { 1s }) |
| 126 | | sltadd1 28025 |
. . . . . . . . . . 11
⊢ ((
0s ∈ No ∧ ({ 0s }
|s { 1s }) ∈ No ∧
1s ∈ No ) → ( 0s
<s ({ 0s } |s { 1s }) ↔ ( 0s
+s 1s ) <s (({ 0s } |s { 1s })
+s 1s ))) |
| 127 | 5, 20, 8, 126 | mp3an 1463 |
. . . . . . . . . 10
⊢ (
0s <s ({ 0s } |s { 1s }) ↔ (
0s +s 1s ) <s (({ 0s } |s {
1s }) +s 1s )) |
| 128 | 125, 127 | mpbi 230 |
. . . . . . . . 9
⊢ (
0s +s 1s ) <s (({ 0s } |s {
1s }) +s 1s ) |
| 129 | 112, 128 | eqbrtrri 5166 |
. . . . . . . 8
⊢
1s <s (({ 0s } |s { 1s }) +s
1s ) |
| 130 | | ovex 7464 |
. . . . . . . . 9
⊢ (({
0s } |s { 1s }) +s 1s ) ∈
V |
| 131 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑦 = (({ 0s } |s {
1s }) +s 1s ) → ( 1s <s
𝑦 ↔ 1s
<s (({ 0s } |s { 1s }) +s 1s
))) |
| 132 | 130, 131 | ralsn 4681 |
. . . . . . . 8
⊢
(∀𝑦 ∈
{(({ 0s } |s { 1s }) +s 1s )}
1s <s 𝑦
↔ 1s <s (({ 0s } |s { 1s })
+s 1s )) |
| 133 | 129, 132 | mpbir 231 |
. . . . . . 7
⊢
∀𝑦 ∈
{(({ 0s } |s { 1s }) +s 1s )}
1s <s 𝑦 |
| 134 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 1s → (
0s <s 𝑥
↔ 0s <s 1s )) |
| 135 | 47, 134 | ralsn 4681 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈ {
1s } 0s <s 𝑥 ↔ 0s <s 1s
) |
| 136 | 13, 135 | mpbir 231 |
. . . . . . . . . . . 12
⊢
∀𝑥 ∈ {
1s } 0s <s 𝑥 |
| 137 | | ral0 4513 |
. . . . . . . . . . . 12
⊢
∀𝑦 ∈
∅ 𝑦 <s ({
0s } |s { 1s }) |
| 138 | | slerec 27864 |
. . . . . . . . . . . . 13
⊢
(((∅ <<s ∅ ∧ { 0s } <<s {
1s }) ∧ ( 0s = (∅ |s ∅) ∧ ({
0s } |s { 1s }) = ({ 0s } |s { 1s
}))) → ( 0s ≤s ({ 0s } |s { 1s })
↔ (∀𝑥 ∈ {
1s } 0s <s 𝑥 ∧ ∀𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s
})))) |
| 139 | 121, 73, 122, 78, 138 | mp4an 693 |
. . . . . . . . . . . 12
⊢ (
0s ≤s ({ 0s } |s { 1s }) ↔
(∀𝑥 ∈ {
1s } 0s <s 𝑥 ∧ ∀𝑦 ∈ ∅ 𝑦 <s ({ 0s } |s { 1s
}))) |
| 140 | 136, 137,
139 | mpbir2an 711 |
. . . . . . . . . . 11
⊢
0s ≤s ({ 0s } |s { 1s }) |
| 141 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑥 = ({ 0s } |s {
1s }) → ( 0s ≤s 𝑥 ↔ 0s ≤s ({ 0s
} |s { 1s }))) |
| 142 | 83, 141 | rexsn 4682 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈ {({
0s } |s { 1s })} 0s ≤s 𝑥 ↔ 0s ≤s ({ 0s
} |s { 1s })) |
| 143 | 140, 142 | mpbir 231 |
. . . . . . . . . 10
⊢
∃𝑥 ∈ {({
0s } |s { 1s })} 0s ≤s 𝑥 |
| 144 | 143 | orci 866 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ {({
0s } |s { 1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )})) |
| 145 | | sltrec 27865 |
. . . . . . . . . 10
⊢
(((∅ <<s ∅ ∧ {({ 0s } |s {
1s })} <<s {(({ 0s } |s { 1s })
+s 1s )}) ∧ ( 0s = (∅ |s ∅)
∧ ({({ 0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) = ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}))) → ( 0s <s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}) ↔ (∃𝑥 ∈ {({ 0s } |s {
1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )})))) |
| 146 | 121, 106,
122, 107, 145 | mp4an 693 |
. . . . . . . . 9
⊢ (
0s <s ({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s )}) ↔
(∃𝑥 ∈ {({
0s } |s { 1s })} 0s ≤s 𝑥 ∨ ∃𝑦 ∈ ∅ 𝑦 ≤s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}))) |
| 147 | 144, 146 | mpbir 231 |
. . . . . . . 8
⊢
0s <s ({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s
)}) |
| 148 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑥 = 0s → (𝑥 <s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}) ↔ 0s <s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}))) |
| 149 | 26, 148 | ralsn 4681 |
. . . . . . . 8
⊢
(∀𝑥 ∈ {
0s }𝑥 <s ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ↔ 0s <s
({({ 0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )})) |
| 150 | 147, 149 | mpbir 231 |
. . . . . . 7
⊢
∀𝑥 ∈ {
0s }𝑥 <s ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) |
| 151 | | slerec 27864 |
. . . . . . . 8
⊢ ((({
0s } <<s ∅ ∧ {({ 0s } |s { 1s
})} <<s {(({ 0s } |s { 1s }) +s
1s )}) ∧ ( 1s = ({ 0s } |s ∅) ∧
({({ 0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) = ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}))) → ( 1s ≤s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )}) ↔ (∀𝑦 ∈ {(({ 0s } |s {
1s }) +s 1s )} 1s <s 𝑦 ∧ ∀𝑥 ∈ { 0s }𝑥 <s ({({ 0s } |s {
1s })} |s {(({ 0s } |s { 1s }) +s
1s )})))) |
| 152 | 77, 106, 79, 107, 151 | mp4an 693 |
. . . . . . 7
⊢ (
1s ≤s ({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s )}) ↔
(∀𝑦 ∈ {(({
0s } |s { 1s }) +s 1s )}
1s <s 𝑦 ∧
∀𝑥 ∈ {
0s }𝑥 <s ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}))) |
| 153 | 133, 150,
152 | mpbir2an 711 |
. . . . . 6
⊢
1s ≤s ({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s
)}) |
| 154 | 105 | scutcld 27848 |
. . . . . . . 8
⊢ (⊤
→ ({({ 0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ∈
No ) |
| 155 | 154 | mptru 1547 |
. . . . . . 7
⊢ ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ∈
No |
| 156 | | sletri3 27800 |
. . . . . . 7
⊢ ((({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ∈
No ∧ 1s ∈ No ) →
(({({ 0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) = 1s ↔ (({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ≤s 1s ∧
1s ≤s ({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s
)})))) |
| 157 | 155, 8, 156 | mp2an 692 |
. . . . . 6
⊢ (({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) = 1s ↔ (({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) ≤s 1s ∧
1s ≤s ({({ 0s } |s { 1s })} |s {(({
0s } |s { 1s }) +s 1s
)}))) |
| 158 | 110, 153,
157 | mpbir2an 711 |
. . . . 5
⊢ ({({
0s } |s { 1s })} |s {(({ 0s } |s {
1s }) +s 1s )}) =
1s |
| 159 | 65, 158 | eqtri 2765 |
. . . 4
⊢ (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
0s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ { 1s }𝑥 = (𝑦 +s ({ 0s } |s {
1s }))} ∪ {𝑥
∣ ∃𝑦 ∈ {
1s }𝑥 = (({
0s } |s { 1s }) +s 𝑦)})) = 1s |
| 160 | 25, 159 | eqtri 2765 |
. . 3
⊢ (({
0s } |s { 1s }) +s ({ 0s } |s {
1s })) = 1s |
| 161 | 22, 160 | eqtri 2765 |
. 2
⊢
(2s ·s ({ 0s } |s {
1s })) = 1s |
| 162 | | 2sno 28403 |
. . . . 5
⊢
2s ∈ No |
| 163 | | 2ne0s 28404 |
. . . . 5
⊢
2s ≠ 0s |
| 164 | 162, 163 | pm3.2i 470 |
. . . 4
⊢
(2s ∈ No ∧
2s ≠ 0s ) |
| 165 | 8, 20, 164 | 3pm3.2i 1340 |
. . 3
⊢ (
1s ∈ No ∧ ({ 0s }
|s { 1s }) ∈ No ∧
(2s ∈ No ∧ 2s
≠ 0s )) |
| 166 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = ({ 0s } |s {
1s }) → (2s ·s 𝑥) = (2s ·s ({
0s } |s { 1s }))) |
| 167 | 166 | eqeq1d 2739 |
. . . . 5
⊢ (𝑥 = ({ 0s } |s {
1s }) → ((2s ·s 𝑥) = 1s ↔ (2s
·s ({ 0s } |s { 1s })) = 1s
)) |
| 168 | 167 | rspcev 3622 |
. . . 4
⊢ ((({
0s } |s { 1s }) ∈ No
∧ (2s ·s ({ 0s } |s { 1s
})) = 1s ) → ∃𝑥 ∈ No
(2s ·s 𝑥) = 1s ) |
| 169 | 20, 161, 168 | mp2an 692 |
. . 3
⊢
∃𝑥 ∈
No (2s ·s 𝑥) =
1s |
| 170 | | divsmulw 28218 |
. . 3
⊢ (((
1s ∈ No ∧ ({ 0s }
|s { 1s }) ∈ No ∧
(2s ∈ No ∧ 2s
≠ 0s )) ∧ ∃𝑥 ∈ No
(2s ·s 𝑥) = 1s ) → (( 1s
/su 2s) = ({ 0s } |s { 1s })
↔ (2s ·s ({ 0s } |s {
1s })) = 1s )) |
| 171 | 165, 169,
170 | mp2an 692 |
. 2
⊢ ((
1s /su 2s) = ({ 0s } |s {
1s }) ↔ (2s ·s ({ 0s }
|s { 1s })) = 1s ) |
| 172 | 161, 171 | mpbir 231 |
1
⊢ (
1s /su 2s) = ({ 0s } |s {
1s }) |