| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0ex 5306 | . . . . 5
⊢ ∅
∈ V | 
| 2 | 1 | elintab 4957 | . . . 4
⊢ (∅
∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥)) | 
| 3 |  | simpl 482 | . . . 4
⊢ ((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥) | 
| 4 | 2, 3 | mpgbir 1798 | . . 3
⊢ ∅
∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} | 
| 5 |  | suceq 6449 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) | 
| 6 | 5 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑦 = 𝑧 → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑧 ∈ 𝑥)) | 
| 7 | 6 | rspccv 3618 | . . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥)) | 
| 8 | 7 | adantl 481 | . . . . . . 7
⊢ ((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥)) | 
| 9 | 8 | a2i 14 | . . . . . 6
⊢
(((∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥)) | 
| 10 | 9 | alimi 1810 | . . . . 5
⊢
(∀𝑥((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥)) | 
| 11 |  | vex 3483 | . . . . . 6
⊢ 𝑧 ∈ V | 
| 12 | 11 | elintab 4957 | . . . . 5
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) | 
| 13 | 11 | sucex 7827 | . . . . . 6
⊢ suc 𝑧 ∈ V | 
| 14 | 13 | elintab 4957 | . . . . 5
⊢ (suc
𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥)) | 
| 15 | 10, 12, 14 | 3imtr4i 292 | . . . 4
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}) | 
| 16 | 15 | rgenw 3064 | . . 3
⊢
∀𝑧 ∈
ω (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}) | 
| 17 |  | peano5 7916 | . . 3
⊢ ((∅
∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ∧ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})) → ω ⊆ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)}) | 
| 18 | 4, 16, 17 | mp2an 692 | . 2
⊢ ω
⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} | 
| 19 |  | peano1 7911 | . . . 4
⊢ ∅
∈ ω | 
| 20 |  | peano2 7913 | . . . . 5
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) | 
| 21 | 20 | rgen 3062 | . . . 4
⊢
∀𝑦 ∈
ω suc 𝑦 ∈
ω | 
| 22 |  | omex 9684 | . . . . . 6
⊢ ω
∈ V | 
| 23 |  | eleq2 2829 | . . . . . . . 8
⊢ (𝑥 = ω → (∅
∈ 𝑥 ↔ ∅
∈ ω)) | 
| 24 |  | eleq2 2829 | . . . . . . . . 9
⊢ (𝑥 = ω → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ ω)) | 
| 25 | 24 | raleqbi1dv 3337 | . . . . . . . 8
⊢ (𝑥 = ω → (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀𝑦 ∈ ω suc 𝑦 ∈ ω)) | 
| 26 | 23, 25 | anbi12d 632 | . . . . . . 7
⊢ (𝑥 = ω → ((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) ↔ (∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈
ω))) | 
| 27 |  | eleq2 2829 | . . . . . . 7
⊢ (𝑥 = ω → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ω)) | 
| 28 | 26, 27 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = ω → (((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈ ω)
→ 𝑧 ∈
ω))) | 
| 29 | 22, 28 | spcv 3604 | . . . . 5
⊢
(∀𝑥((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈ ω)
→ 𝑧 ∈
ω)) | 
| 30 | 12, 29 | sylbi 217 | . . . 4
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → ((∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈ ω)
→ 𝑧 ∈
ω)) | 
| 31 | 19, 21, 30 | mp2ani 698 | . . 3
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → 𝑧 ∈ ω) | 
| 32 | 31 | ssriv 3986 | . 2
⊢ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} ⊆ ω | 
| 33 | 18, 32 | eqssi 3999 | 1
⊢ ω =
∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |