Step | Hyp | Ref
| Expression |
1 | | 0ex 5235 |
. . . . 5
⊢ ∅
∈ V |
2 | 1 | elintab 4896 |
. . . 4
⊢ (∅
∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥)) |
3 | | simpl 483 |
. . . 4
⊢ ((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → ∅ ∈ 𝑥) |
4 | 2, 3 | mpgbir 1806 |
. . 3
⊢ ∅
∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
5 | | suceq 6330 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) |
6 | 5 | eleq1d 2825 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑧 ∈ 𝑥)) |
7 | 6 | rspccv 3558 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥 → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥)) |
8 | 7 | adantl 482 |
. . . . . . 7
⊢ ((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → (𝑧 ∈ 𝑥 → suc 𝑧 ∈ 𝑥)) |
9 | 8 | a2i 14 |
. . . . . 6
⊢
(((∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥)) |
10 | 9 | alimi 1818 |
. . . . 5
⊢
(∀𝑥((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥)) |
11 | | vex 3435 |
. . . . . 6
⊢ 𝑧 ∈ V |
12 | 11 | elintab 4896 |
. . . . 5
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥)) |
13 | 11 | sucex 7650 |
. . . . . 6
⊢ suc 𝑧 ∈ V |
14 | 13 | elintab 4896 |
. . . . 5
⊢ (suc
𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} ↔ ∀𝑥((∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → suc 𝑧 ∈ 𝑥)) |
15 | 10, 12, 14 | 3imtr4i 292 |
. . . 4
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}) |
16 | 15 | rgenw 3078 |
. . 3
⊢
∀𝑧 ∈
ω (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)}) |
17 | | peano5 7734 |
. . 3
⊢ ((∅
∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} ∧ ∀𝑧 ∈ ω (𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} → suc 𝑧 ∈ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)})) → ω ⊆ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)}) |
18 | 4, 16, 17 | mp2an 689 |
. 2
⊢ ω
⊆ ∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |
19 | | peano1 7729 |
. . . 4
⊢ ∅
∈ ω |
20 | | peano2 7731 |
. . . . 5
⊢ (𝑦 ∈ ω → suc 𝑦 ∈
ω) |
21 | 20 | rgen 3076 |
. . . 4
⊢
∀𝑦 ∈
ω suc 𝑦 ∈
ω |
22 | | omex 9379 |
. . . . . 6
⊢ ω
∈ V |
23 | | eleq2 2829 |
. . . . . . . 8
⊢ (𝑥 = ω → (∅
∈ 𝑥 ↔ ∅
∈ ω)) |
24 | | eleq2 2829 |
. . . . . . . . 9
⊢ (𝑥 = ω → (suc 𝑦 ∈ 𝑥 ↔ suc 𝑦 ∈ ω)) |
25 | 24 | raleqbi1dv 3339 |
. . . . . . . 8
⊢ (𝑥 = ω → (∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥 ↔ ∀𝑦 ∈ ω suc 𝑦 ∈ ω)) |
26 | 23, 25 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = ω → ((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) ↔ (∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈
ω))) |
27 | | eleq2 2829 |
. . . . . . 7
⊢ (𝑥 = ω → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ ω)) |
28 | 26, 27 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = ω → (((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) ↔ ((∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈ ω)
→ 𝑧 ∈
ω))) |
29 | 22, 28 | spcv 3543 |
. . . . 5
⊢
(∀𝑥((∅
∈ 𝑥 ∧
∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥) → 𝑧 ∈ 𝑥) → ((∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈ ω)
→ 𝑧 ∈
ω)) |
30 | 12, 29 | sylbi 216 |
. . . 4
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → ((∅ ∈ ω ∧
∀𝑦 ∈ ω
suc 𝑦 ∈ ω)
→ 𝑧 ∈
ω)) |
31 | 19, 21, 30 | mp2ani 695 |
. . 3
⊢ (𝑧 ∈ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} → 𝑧 ∈ ω) |
32 | 31 | ssriv 3930 |
. 2
⊢ ∩ {𝑥
∣ (∅ ∈ 𝑥
∧ ∀𝑦 ∈
𝑥 suc 𝑦 ∈ 𝑥)} ⊆ ω |
33 | 18, 32 | eqssi 3942 |
1
⊢ ω =
∩ {𝑥 ∣ (∅ ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 suc 𝑦 ∈ 𝑥)} |