| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0sno 27872 | . . . . . 6
⊢ 
0s ∈  No | 
| 2 | 1 | elexi 3502 | . . . . 5
⊢ 
0s ∈ V | 
| 3 | 2 | elintab 4957 | . . . 4
⊢ (
0s ∈ ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ↔ ∀𝑥(( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥) → 0s ∈
𝑥)) | 
| 4 |  | simpl 482 | . . . 4
⊢ ((
0s ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 (𝑦 +s 1s ) ∈ 𝑥) → 0s ∈
𝑥) | 
| 5 | 3, 4 | mpgbir 1798 | . . 3
⊢ 
0s ∈ ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} | 
| 6 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (𝑦 +s 1s ) = (𝑧 +s 1s
)) | 
| 7 | 6 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝑦 +s 1s ) ∈ 𝑥 ↔ (𝑧 +s 1s ) ∈ 𝑥)) | 
| 8 | 7 | rspccv 3618 | . . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 (𝑦 +s 1s ) ∈ 𝑥 → (𝑧 ∈ 𝑥 → (𝑧 +s 1s ) ∈ 𝑥)) | 
| 9 | 8 | adantl 481 | . . . . . . 7
⊢ ((
0s ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 (𝑦 +s 1s ) ∈ 𝑥) → (𝑧 ∈ 𝑥 → (𝑧 +s 1s ) ∈ 𝑥)) | 
| 10 | 9 | a2i 14 | . . . . . 6
⊢ (((
0s ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 (𝑦 +s 1s ) ∈ 𝑥) → 𝑧 ∈ 𝑥) → (( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥) → (𝑧 +s 1s ) ∈ 𝑥)) | 
| 11 | 10 | alimi 1810 | . . . . 5
⊢
(∀𝑥((
0s ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 (𝑦 +s 1s ) ∈ 𝑥) → 𝑧 ∈ 𝑥) → ∀𝑥(( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥) → (𝑧 +s 1s ) ∈ 𝑥)) | 
| 12 |  | vex 3483 | . . . . . 6
⊢ 𝑧 ∈ V | 
| 13 | 12 | elintab 4957 | . . . . 5
⊢ (𝑧 ∈ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ↔ ∀𝑥(( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥) → 𝑧 ∈ 𝑥)) | 
| 14 |  | ovex 7465 | . . . . . 6
⊢ (𝑧 +s 1s )
∈ V | 
| 15 | 14 | elintab 4957 | . . . . 5
⊢ ((𝑧 +s 1s )
∈ ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ↔ ∀𝑥(( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥) → (𝑧 +s 1s ) ∈ 𝑥)) | 
| 16 | 11, 13, 15 | 3imtr4i 292 | . . . 4
⊢ (𝑧 ∈ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} → (𝑧 +s 1s ) ∈ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}) | 
| 17 | 16 | rgen 3062 | . . 3
⊢
∀𝑧 ∈
∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} (𝑧 +s 1s ) ∈ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} | 
| 18 |  | peano5n0s 28325 | . . 3
⊢ ((
0s ∈ ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ∧ ∀𝑧 ∈ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} (𝑧 +s 1s ) ∈ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}) → ℕ0s
⊆ ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}) | 
| 19 | 5, 17, 18 | mp2an 692 | . 2
⊢
ℕ0s ⊆ ∩ {𝑥 ∣ ( 0s ∈
𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} | 
| 20 |  | 0n0s 28335 | . . . 4
⊢ 
0s ∈ ℕ0s | 
| 21 |  | peano2n0s 28336 | . . . . 5
⊢ (𝑦 ∈ ℕ0s
→ (𝑦 +s
1s ) ∈ ℕ0s) | 
| 22 | 21 | rgen 3062 | . . . 4
⊢
∀𝑦 ∈
ℕ0s (𝑦
+s 1s ) ∈ ℕ0s | 
| 23 |  | n0sex 28323 | . . . . 5
⊢
ℕ0s ∈ V | 
| 24 |  | eleq2 2829 | . . . . . 6
⊢ (𝑥 = ℕ0s → (
0s ∈ 𝑥
↔ 0s ∈ ℕ0s)) | 
| 25 |  | eleq2 2829 | . . . . . . 7
⊢ (𝑥 = ℕ0s →
((𝑦 +s
1s ) ∈ 𝑥
↔ (𝑦 +s
1s ) ∈ ℕ0s)) | 
| 26 | 25 | raleqbi1dv 3337 | . . . . . 6
⊢ (𝑥 = ℕ0s →
(∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥 ↔ ∀𝑦 ∈ ℕ0s
(𝑦 +s
1s ) ∈ ℕ0s)) | 
| 27 | 24, 26 | anbi12d 632 | . . . . 5
⊢ (𝑥 = ℕ0s →
(( 0s ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 (𝑦 +s 1s ) ∈ 𝑥) ↔ ( 0s ∈
ℕ0s ∧ ∀𝑦 ∈ ℕ0s (𝑦 +s 1s )
∈ ℕ0s))) | 
| 28 | 23, 27 | elab 3678 | . . . 4
⊢
(ℕ0s ∈ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ↔ ( 0s ∈
ℕ0s ∧ ∀𝑦 ∈ ℕ0s (𝑦 +s 1s )
∈ ℕ0s)) | 
| 29 | 20, 22, 28 | mpbir2an 711 | . . 3
⊢
ℕ0s ∈ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} | 
| 30 |  | intss1 4962 | . . 3
⊢
(ℕ0s ∈ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} → ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ⊆
ℕ0s) | 
| 31 | 29, 30 | ax-mp 5 | . 2
⊢ ∩ {𝑥
∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} ⊆
ℕ0s | 
| 32 | 19, 31 | eqssi 3999 | 1
⊢
ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} |