Step | Hyp | Ref
| Expression |
1 | | bj-dfom 10057 |
. . . 4
⊢ ω =
∩ {𝑦 ∣ Ind 𝑦} |
2 | | peano1 4317 |
. . . . . . . . . . 11
⊢ ∅
∈ ω |
3 | | elin 3126 |
. . . . . . . . . . 11
⊢ (∅
∈ (ω ∩ 𝐴)
↔ (∅ ∈ ω ∧ ∅ ∈ 𝐴)) |
4 | 2, 3 | mpbiran 847 |
. . . . . . . . . 10
⊢ (∅
∈ (ω ∩ 𝐴)
↔ ∅ ∈ 𝐴) |
5 | 4 | biimpri 124 |
. . . . . . . . 9
⊢ (∅
∈ 𝐴 → ∅
∈ (ω ∩ 𝐴)) |
6 | | bj-peano2 10063 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
7 | 6 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ ω) |
8 | 7 | a1i 9 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ ω)) |
9 | | pm3.31 249 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → suc 𝑥 ∈ 𝐴)) |
10 | 8, 9 | jcad 291 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
11 | 10 | alimi 1344 |
. . . . . . . . . . 11
⊢
(∀𝑥(𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ∀𝑥((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
12 | | df-ral 2311 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) ↔ ∀𝑥(𝑥 ∈ ω → (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) |
13 | | elin 3126 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (ω ∩ 𝐴) ↔ (𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴)) |
14 | | elin 3126 |
. . . . . . . . . . . . 13
⊢ (suc
𝑥 ∈ (ω ∩
𝐴) ↔ (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴)) |
15 | 13, 14 | imbi12i 228 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴)) ↔ ((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
16 | 15 | albii 1359 |
. . . . . . . . . . 11
⊢
(∀𝑥(𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴)) ↔ ∀𝑥((𝑥 ∈ ω ∧ 𝑥 ∈ 𝐴) → (suc 𝑥 ∈ ω ∧ suc 𝑥 ∈ 𝐴))) |
17 | 11, 12, 16 | 3imtr4i 190 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → ∀𝑥(𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴))) |
18 | | df-ral 2311 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴) ↔ ∀𝑥(𝑥 ∈ (ω ∩ 𝐴) → suc 𝑥 ∈ (ω ∩ 𝐴))) |
19 | 17, 18 | sylibr 137 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴) → ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴)) |
20 | 5, 19 | anim12i 321 |
. . . . . . . 8
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (∅ ∈ (ω ∩
𝐴) ∧ ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴))) |
21 | | df-bj-ind 10051 |
. . . . . . . 8
⊢ (Ind
(ω ∩ 𝐴) ↔
(∅ ∈ (ω ∩ 𝐴) ∧ ∀𝑥 ∈ (ω ∩ 𝐴)suc 𝑥 ∈ (ω ∩ 𝐴))) |
22 | 20, 21 | sylibr 137 |
. . . . . . 7
⊢ ((∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → Ind (ω ∩ 𝐴)) |
23 | | bj-indeq 10053 |
. . . . . . . 8
⊢ (𝑦 = (ω ∩ 𝐴) → (Ind 𝑦 ↔ Ind (ω ∩ 𝐴))) |
24 | 23 | elabg 2688 |
. . . . . . 7
⊢ ((ω
∩ 𝐴) ∈ 𝑉 → ((ω ∩ 𝐴) ∈ {𝑦 ∣ Ind 𝑦} ↔ Ind (ω ∩ 𝐴))) |
25 | 22, 24 | syl5ibr 145 |
. . . . . 6
⊢ ((ω
∩ 𝐴) ∈ 𝑉 → ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → (ω ∩ 𝐴) ∈ {𝑦 ∣ Ind 𝑦})) |
26 | 25 | imp 115 |
. . . . 5
⊢
(((ω ∩ 𝐴)
∈ 𝑉 ∧ (∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) → (ω ∩ 𝐴) ∈ {𝑦 ∣ Ind 𝑦}) |
27 | | intss1 3630 |
. . . . 5
⊢ ((ω
∩ 𝐴) ∈ {𝑦 ∣ Ind 𝑦} → ∩ {𝑦 ∣ Ind 𝑦} ⊆ (ω ∩ 𝐴)) |
28 | 26, 27 | syl 14 |
. . . 4
⊢
(((ω ∩ 𝐴)
∈ 𝑉 ∧ (∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) → ∩
{𝑦 ∣ Ind 𝑦} ⊆ (ω ∩ 𝐴)) |
29 | 1, 28 | syl5eqss 2989 |
. . 3
⊢
(((ω ∩ 𝐴)
∈ 𝑉 ∧ (∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) → ω ⊆ (ω ∩
𝐴)) |
30 | | inss2 3158 |
. . 3
⊢ (ω
∩ 𝐴) ⊆ 𝐴 |
31 | 29, 30 | syl6ss 2957 |
. 2
⊢
(((ω ∩ 𝐴)
∈ 𝑉 ∧ (∅
∈ 𝐴 ∧
∀𝑥 ∈ ω
(𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴))) → ω ⊆ 𝐴) |
32 | 31 | ex 108 |
1
⊢ ((ω
∩ 𝐴) ∈ 𝑉 → ((∅ ∈ 𝐴 ∧ ∀𝑥 ∈ ω (𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴)) → ω ⊆ 𝐴)) |