Step | Hyp | Ref
| Expression |
1 | | dfom3 4576 |
. . 3
⊢ ω =
∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} |
2 | | peano1 4578 |
. . . . . . . 8
⊢ ∅
∈ ω |
3 | | elin 3310 |
. . . . . . . 8
⊢ (∅
∈ (ω ∩ 𝐴)
↔ (∅ ∈ ω ∧ ∅ ∈ 𝐴)) |
4 | 2, 3 | mpbiran 935 |
. . . . . . 7
⊢ (∅
∈ (ω ∩ 𝐴)
↔ ∅ ∈ 𝐴) |
5 | 4 | biimpri 132 |
. . . . . 6
⊢ (∅
∈ 𝐴 → ∅
∈ (ω ∩ 𝐴)) |
6 | | peano2 4579 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
7 | 6 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ ω) |
8 | 7 | a1i 9 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ ω)) |
9 | | pm3.31 260 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ 𝐴)) |
10 | 8, 9 | jcad 305 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
11 | 10 | alimi 1448 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ∀𝑥((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
12 | | df-ral 2453 |
. . . . . . . 8
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) |
13 | | elin 3310 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ω ∩ 𝐴) ↔ (𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴)) |
14 | | elin 3310 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ (ω ∩
𝐴) ↔ (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴)) |
15 | 13, 14 | imbi12i 238 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴)) ↔ ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
16 | 15 | albii 1463 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴)) ↔ ∀𝑥((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
17 | 11, 12, 16 | 3imtr4i 200 |
. . . . . . 7
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → ∀𝑥(𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴))) |
18 | | df-ral 2453 |
. . . . . . 7
⊢
(∀𝑥 ∈
(ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴) ↔ ∀𝑥(𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴))) |
19 | 17, 18 | sylibr 133 |
. . . . . 6
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴)) |
20 | 5, 19 | anim12i 336 |
. . . . 5
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (∅ ∈ (ω ∩
𝐴) ∧ ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴))) |
21 | | omex 4577 |
. . . . . . 7
⊢ ω
∈ V |
22 | 21 | inex1 4123 |
. . . . . 6
⊢ (ω
∩ 𝐴) ∈
V |
23 | | eleq2 2234 |
. . . . . . 7
⊢ (𝑦 = (ω ∩ 𝐴) → (∅ ∈ 𝑦 ↔ ∅ ∈ (ω
∩ 𝐴))) |
24 | | eleq2 2234 |
. . . . . . . 8
⊢ (𝑦 = (ω ∩ 𝐴) → (suc 𝑥 ∈ 𝑦 ↔ suc 𝑥 ∈ (ω ∩ 𝐴))) |
25 | 24 | raleqbi1dv 2673 |
. . . . . . 7
⊢ (𝑦 = (ω ∩ 𝐴) → (∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦 ↔ ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴))) |
26 | 23, 25 | anbi12d 470 |
. . . . . 6
⊢ (𝑦 = (ω ∩ 𝐴) → ((∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦) ↔ (∅ ∈ (ω ∩ 𝐴) ∧ ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴)))) |
27 | 22, 26 | elab 2874 |
. . . . 5
⊢ ((ω
∩ 𝐴) ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ↔ (∅ ∈ (ω ∩
𝐴) ∧ ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴))) |
28 | 20, 27 | sylibr 133 |
. . . 4
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (ω ∩ 𝐴) ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)}) |
29 | | intss1 3846 |
. . . 4
⊢ ((ω
∩ 𝐴) ∈ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} → ∩ {𝑦 ∣ (∅ ∈ 𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ⊆ (ω ∩ 𝐴)) |
30 | 28, 29 | syl 14 |
. . 3
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ∩
{𝑦 ∣ (∅ ∈
𝑦 ∧ ∀𝑥 ∈ 𝑦 suc 𝑥 ∈ 𝑦)} ⊆ (ω ∩ 𝐴)) |
31 | 1, 30 | eqsstrid 3193 |
. 2
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ (ω ∩
𝐴)) |
32 | | ssid 3167 |
. . . 4
⊢ ω
⊆ ω |
33 | 32 | biantrur 301 |
. . 3
⊢ (ω
⊆ 𝐴 ↔ (ω
⊆ ω ∧ ω ⊆ 𝐴)) |
34 | | ssin 3349 |
. . 3
⊢ ((ω
⊆ ω ∧ ω ⊆ 𝐴) ↔ ω ⊆ (ω ∩
𝐴)) |
35 | 33, 34 | bitri 183 |
. 2
⊢ (ω
⊆ 𝐴 ↔ ω
⊆ (ω ∩ 𝐴)) |
36 | 31, 35 | sylibr 133 |
1
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴) |