| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqeq1 2740 | . . 3
⊢ (𝑦 = 0s → (𝑦 = 0s ↔
0s = 0s )) | 
| 2 |  | eqeq1 2740 | . . . 4
⊢ (𝑦 = 0s → (𝑦 = (𝑥 +s 1s ) ↔
0s = (𝑥
+s 1s ))) | 
| 3 | 2 | rexbidv 3178 | . . 3
⊢ (𝑦 = 0s →
(∃𝑥 ∈
ℕ0s 𝑦 =
(𝑥 +s
1s ) ↔ ∃𝑥 ∈ ℕ0s 0s =
(𝑥 +s
1s ))) | 
| 4 | 1, 3 | orbi12d 918 | . 2
⊢ (𝑦 = 0s → ((𝑦 = 0s ∨
∃𝑥 ∈
ℕ0s 𝑦 =
(𝑥 +s
1s )) ↔ ( 0s = 0s ∨ ∃𝑥 ∈ ℕ0s
0s = (𝑥
+s 1s )))) | 
| 5 |  | eqeq1 2740 | . . 3
⊢ (𝑦 = 𝑧 → (𝑦 = 0s ↔ 𝑧 = 0s )) | 
| 6 |  | eqeq1 2740 | . . . 4
⊢ (𝑦 = 𝑧 → (𝑦 = (𝑥 +s 1s ) ↔ 𝑧 = (𝑥 +s 1s
))) | 
| 7 | 6 | rexbidv 3178 | . . 3
⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ ℕ0s 𝑦 = (𝑥 +s 1s ) ↔
∃𝑥 ∈
ℕ0s 𝑧 =
(𝑥 +s
1s ))) | 
| 8 | 5, 7 | orbi12d 918 | . 2
⊢ (𝑦 = 𝑧 → ((𝑦 = 0s ∨ ∃𝑥 ∈ ℕ0s
𝑦 = (𝑥 +s 1s )) ↔ (𝑧 = 0s ∨
∃𝑥 ∈
ℕ0s 𝑧 =
(𝑥 +s
1s )))) | 
| 9 |  | eqeq1 2740 | . . 3
⊢ (𝑦 = (𝑧 +s 1s ) → (𝑦 = 0s ↔ (𝑧 +s 1s ) =
0s )) | 
| 10 |  | eqeq1 2740 | . . . 4
⊢ (𝑦 = (𝑧 +s 1s ) → (𝑦 = (𝑥 +s 1s ) ↔ (𝑧 +s 1s ) =
(𝑥 +s
1s ))) | 
| 11 | 10 | rexbidv 3178 | . . 3
⊢ (𝑦 = (𝑧 +s 1s ) →
(∃𝑥 ∈
ℕ0s 𝑦 =
(𝑥 +s
1s ) ↔ ∃𝑥 ∈ ℕ0s (𝑧 +s 1s ) =
(𝑥 +s
1s ))) | 
| 12 | 9, 11 | orbi12d 918 | . 2
⊢ (𝑦 = (𝑧 +s 1s ) → ((𝑦 = 0s ∨
∃𝑥 ∈
ℕ0s 𝑦 =
(𝑥 +s
1s )) ↔ ((𝑧
+s 1s ) = 0s ∨ ∃𝑥 ∈ ℕ0s (𝑧 +s 1s ) =
(𝑥 +s
1s )))) | 
| 13 |  | eqeq1 2740 | . . 3
⊢ (𝑦 = 𝐴 → (𝑦 = 0s ↔ 𝐴 = 0s )) | 
| 14 |  | eqeq1 2740 | . . . 4
⊢ (𝑦 = 𝐴 → (𝑦 = (𝑥 +s 1s ) ↔ 𝐴 = (𝑥 +s 1s
))) | 
| 15 | 14 | rexbidv 3178 | . . 3
⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ ℕ0s 𝑦 = (𝑥 +s 1s ) ↔
∃𝑥 ∈
ℕ0s 𝐴 =
(𝑥 +s
1s ))) | 
| 16 | 13, 15 | orbi12d 918 | . 2
⊢ (𝑦 = 𝐴 → ((𝑦 = 0s ∨ ∃𝑥 ∈ ℕ0s
𝑦 = (𝑥 +s 1s )) ↔ (𝐴 = 0s ∨
∃𝑥 ∈
ℕ0s 𝐴 =
(𝑥 +s
1s )))) | 
| 17 |  | eqid 2736 | . . 3
⊢ 
0s = 0s | 
| 18 | 17 | orci 865 | . 2
⊢ (
0s = 0s ∨ ∃𝑥 ∈ ℕ0s 0s =
(𝑥 +s
1s )) | 
| 19 |  | clel5 3664 | . . . . . 6
⊢ (𝑧 ∈ ℕ0s
↔ ∃𝑥 ∈
ℕ0s 𝑧 =
𝑥) | 
| 20 | 19 | biimpi 216 | . . . . 5
⊢ (𝑧 ∈ ℕ0s
→ ∃𝑥 ∈
ℕ0s 𝑧 =
𝑥) | 
| 21 |  | n0sno 28329 | . . . . . . 7
⊢ (𝑧 ∈ ℕ0s
→ 𝑧 ∈  No ) | 
| 22 |  | n0sno 28329 | . . . . . . 7
⊢ (𝑥 ∈ ℕ0s
→ 𝑥 ∈  No ) | 
| 23 |  | 1sno 27873 | . . . . . . . 8
⊢ 
1s ∈  No | 
| 24 |  | addscan2 28027 | . . . . . . . 8
⊢ ((𝑧 ∈ 
No  ∧ 𝑥 ∈
 No  ∧ 1s ∈  No ) → ((𝑧 +s 1s ) = (𝑥 +s 1s )
↔ 𝑧 = 𝑥)) | 
| 25 | 23, 24 | mp3an3 1451 | . . . . . . 7
⊢ ((𝑧 ∈ 
No  ∧ 𝑥 ∈
 No ) → ((𝑧 +s 1s ) = (𝑥 +s 1s )
↔ 𝑧 = 𝑥)) | 
| 26 | 21, 22, 25 | syl2an 596 | . . . . . 6
⊢ ((𝑧 ∈ ℕ0s
∧ 𝑥 ∈
ℕ0s) → ((𝑧 +s 1s ) = (𝑥 +s 1s )
↔ 𝑧 = 𝑥)) | 
| 27 | 26 | rexbidva 3176 | . . . . 5
⊢ (𝑧 ∈ ℕ0s
→ (∃𝑥 ∈
ℕ0s (𝑧
+s 1s ) = (𝑥 +s 1s ) ↔
∃𝑥 ∈
ℕ0s 𝑧 =
𝑥)) | 
| 28 | 20, 27 | mpbird 257 | . . . 4
⊢ (𝑧 ∈ ℕ0s
→ ∃𝑥 ∈
ℕ0s (𝑧
+s 1s ) = (𝑥 +s 1s
)) | 
| 29 | 28 | olcd 874 | . . 3
⊢ (𝑧 ∈ ℕ0s
→ ((𝑧 +s
1s ) = 0s ∨ ∃𝑥 ∈ ℕ0s (𝑧 +s 1s ) =
(𝑥 +s
1s ))) | 
| 30 | 29 | a1d 25 | . 2
⊢ (𝑧 ∈ ℕ0s
→ ((𝑧 = 0s
∨ ∃𝑥 ∈
ℕ0s 𝑧 =
(𝑥 +s
1s )) → ((𝑧
+s 1s ) = 0s ∨ ∃𝑥 ∈ ℕ0s (𝑧 +s 1s ) =
(𝑥 +s
1s )))) | 
| 31 | 4, 8, 12, 16, 18, 30 | n0sind 28338 | 1
⊢ (𝐴 ∈ ℕ0s
→ (𝐴 = 0s
∨ ∃𝑥 ∈
ℕ0s 𝐴 =
(𝑥 +s
1s ))) |