| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0sno 27871 | . . . . . . . . . 10
⊢ 
0s ∈  No | 
| 2 | 1 | elexi 3503 | . . . . . . . . 9
⊢ 
0s ∈ V | 
| 3 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑦 = 0s → (𝑦 +s 1s ) =
( 0s +s 1s )) | 
| 4 | 3 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑦 = 0s → (𝑥 = (𝑦 +s 1s ) ↔ 𝑥 = ( 0s +s
1s ))) | 
| 5 | 2, 4 | rexsn 4682 | . . . . . . . 8
⊢
(∃𝑦 ∈ {
0s }𝑥 = (𝑦 +s 1s )
↔ 𝑥 = ( 0s
+s 1s )) | 
| 6 |  | 1sno 27872 | . . . . . . . . . 10
⊢ 
1s ∈  No | 
| 7 |  | addslid 28001 | . . . . . . . . . 10
⊢ (
1s ∈  No  → ( 0s
+s 1s ) = 1s ) | 
| 8 | 6, 7 | ax-mp 5 | . . . . . . . . 9
⊢ (
0s +s 1s ) = 1s | 
| 9 | 8 | eqeq2i 2750 | . . . . . . . 8
⊢ (𝑥 = ( 0s +s
1s ) ↔ 𝑥 =
1s ) | 
| 10 | 5, 9 | bitri 275 | . . . . . . 7
⊢
(∃𝑦 ∈ {
0s }𝑥 = (𝑦 +s 1s )
↔ 𝑥 = 1s
) | 
| 11 | 10 | abbii 2809 | . . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} = {𝑥 ∣ 𝑥 = 1s } | 
| 12 |  | df-sn 4627 | . . . . . 6
⊢ {
1s } = {𝑥
∣ 𝑥 = 1s
} | 
| 13 | 11, 12 | eqtr4i 2768 | . . . . 5
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} = {
1s } | 
| 14 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑦 = 0s → (
1s +s 𝑦) = ( 1s +s
0s )) | 
| 15 | 14 | eqeq2d 2748 | . . . . . . . . 9
⊢ (𝑦 = 0s → (𝑥 = ( 1s +s
𝑦) ↔ 𝑥 = ( 1s +s
0s ))) | 
| 16 | 2, 15 | rexsn 4682 | . . . . . . . 8
⊢
(∃𝑦 ∈ {
0s }𝑥 = (
1s +s 𝑦) ↔ 𝑥 = ( 1s +s
0s )) | 
| 17 |  | addsrid 27997 | . . . . . . . . . 10
⊢ (
1s ∈  No  → ( 1s
+s 0s ) = 1s ) | 
| 18 | 6, 17 | ax-mp 5 | . . . . . . . . 9
⊢ (
1s +s 0s ) = 1s | 
| 19 | 18 | eqeq2i 2750 | . . . . . . . 8
⊢ (𝑥 = ( 1s +s
0s ) ↔ 𝑥 =
1s ) | 
| 20 | 16, 19 | bitri 275 | . . . . . . 7
⊢
(∃𝑦 ∈ {
0s }𝑥 = (
1s +s 𝑦) ↔ 𝑥 = 1s ) | 
| 21 | 20 | abbii 2809 | . . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)} = {𝑥 ∣ 𝑥 = 1s } | 
| 22 | 21, 12 | eqtr4i 2768 | . . . . 5
⊢ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)} = { 1s
} | 
| 23 | 13, 22 | uneq12i 4166 | . . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)}) = ({ 1s }
∪ { 1s }) | 
| 24 |  | unidm 4157 | . . . 4
⊢ ({
1s } ∪ { 1s }) = { 1s } | 
| 25 | 23, 24 | eqtri 2765 | . . 3
⊢ ({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)}) = { 1s
} | 
| 26 |  | rex0 4360 | . . . . . 6
⊢  ¬
∃𝑦 ∈ ∅
𝑥 = (𝑦 +s 1s
) | 
| 27 | 26 | abf 4406 | . . . . 5
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 1s )} =
∅ | 
| 28 |  | rex0 4360 | . . . . . 6
⊢  ¬
∃𝑦 ∈ ∅
𝑥 = ( 1s
+s 𝑦) | 
| 29 | 28 | abf 4406 | . . . . 5
⊢ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = ( 1s +s
𝑦)} =
∅ | 
| 30 | 27, 29 | uneq12i 4166 | . . . 4
⊢ ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = ( 1s +s
𝑦)}) = (∅ ∪
∅) | 
| 31 |  | unidm 4157 | . . . 4
⊢ (∅
∪ ∅) = ∅ | 
| 32 | 30, 31 | eqtri 2765 | . . 3
⊢ ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = ( 1s +s
𝑦)}) =
∅ | 
| 33 | 25, 32 | oveq12i 7443 | . 2
⊢ (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = ( 1s +s
𝑦)})) = ({ 1s }
|s ∅) | 
| 34 |  | snelpwi 5448 | . . . . . . 7
⊢ (
0s ∈  No  → { 0s }
∈ 𝒫  No ) | 
| 35 | 1, 34 | ax-mp 5 | . . . . . 6
⊢ {
0s } ∈ 𝒫  No | 
| 36 |  | nulssgt 27843 | . . . . . 6
⊢ ({
0s } ∈ 𝒫  No  → {
0s } <<s ∅) | 
| 37 | 35, 36 | ax-mp 5 | . . . . 5
⊢ {
0s } <<s ∅ | 
| 38 | 37 | a1i 11 | . . . 4
⊢ (⊤
→ { 0s } <<s ∅) | 
| 39 |  | df-1s 27870 | . . . . 5
⊢ 
1s = ({ 0s } |s ∅) | 
| 40 | 39 | a1i 11 | . . . 4
⊢ (⊤
→ 1s = ({ 0s } |s ∅)) | 
| 41 | 38, 38, 40, 40 | addsunif 28035 | . . 3
⊢ (⊤
→ ( 1s +s 1s ) = (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = ( 1s +s
𝑦)}))) | 
| 42 | 41 | mptru 1547 | . 2
⊢ (
1s +s 1s ) = (({𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ { 0s }𝑥 = ( 1s +s
𝑦)}) |s ({𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = (𝑦 +s 1s )} ∪ {𝑥 ∣ ∃𝑦 ∈ ∅ 𝑥 = ( 1s +s
𝑦)})) | 
| 43 |  | df-2s 28395 | . 2
⊢
2s = ({ 1s } |s ∅) | 
| 44 | 33, 42, 43 | 3eqtr4i 2775 | 1
⊢ (
1s +s 1s ) = 2s |