Step | Hyp | Ref
| Expression |
1 | | bj-omex 11022 |
. . 3
⊢ ω
∈ V |
2 | | sseq2 3030 |
. . . . . 6
⊢ (𝑎 = ω → (𝑦 ⊆ 𝑎 ↔ 𝑦 ⊆ ω)) |
3 | | sseq2 3030 |
. . . . . 6
⊢ (𝑎 = ω → (suc 𝑦 ⊆ 𝑎 ↔ suc 𝑦 ⊆ ω)) |
4 | 2, 3 | imbi12d 232 |
. . . . 5
⊢ (𝑎 = ω → ((𝑦 ⊆ 𝑎 → suc 𝑦 ⊆ 𝑎) ↔ (𝑦 ⊆ ω → suc 𝑦 ⊆
ω))) |
5 | 4 | ralbidv 2373 |
. . . 4
⊢ (𝑎 = ω → (∀𝑦 ∈ ω (𝑦 ⊆ 𝑎 → suc 𝑦 ⊆ 𝑎) ↔ ∀𝑦 ∈ ω (𝑦 ⊆ ω → suc 𝑦 ⊆
ω))) |
6 | | sseq2 3030 |
. . . . 5
⊢ (𝑎 = ω → (𝐴 ⊆ 𝑎 ↔ 𝐴 ⊆ ω)) |
7 | 6 | imbi2d 228 |
. . . 4
⊢ (𝑎 = ω → ((𝐴 ∈ ω → 𝐴 ⊆ 𝑎) ↔ (𝐴 ∈ ω → 𝐴 ⊆ ω))) |
8 | 5, 7 | imbi12d 232 |
. . 3
⊢ (𝑎 = ω →
((∀𝑦 ∈ ω
(𝑦 ⊆ 𝑎 → suc 𝑦 ⊆ 𝑎) → (𝐴 ∈ ω → 𝐴 ⊆ 𝑎)) ↔ (∀𝑦 ∈ ω (𝑦 ⊆ ω → suc 𝑦 ⊆ ω) → (𝐴 ∈ ω → 𝐴 ⊆
ω)))) |
9 | | 0ss 3298 |
. . . 4
⊢ ∅
⊆ 𝑎 |
10 | | bdcv 10924 |
. . . . . 6
⊢
BOUNDED 𝑎 |
11 | 10 | bdss 10940 |
. . . . 5
⊢
BOUNDED 𝑥 ⊆ 𝑎 |
12 | | nfv 1462 |
. . . . 5
⊢
Ⅎ𝑥∅
⊆ 𝑎 |
13 | | nfv 1462 |
. . . . 5
⊢
Ⅎ𝑥 𝑦 ⊆ 𝑎 |
14 | | nfv 1462 |
. . . . 5
⊢
Ⅎ𝑥 suc 𝑦 ⊆ 𝑎 |
15 | | sseq1 3029 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ⊆ 𝑎 ↔ ∅ ⊆ 𝑎)) |
16 | 15 | biimprd 156 |
. . . . 5
⊢ (𝑥 = ∅ → (∅
⊆ 𝑎 → 𝑥 ⊆ 𝑎)) |
17 | | sseq1 3029 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝑎 ↔ 𝑦 ⊆ 𝑎)) |
18 | 17 | biimpd 142 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥 ⊆ 𝑎 → 𝑦 ⊆ 𝑎)) |
19 | | sseq1 3029 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑥 ⊆ 𝑎 ↔ suc 𝑦 ⊆ 𝑎)) |
20 | 19 | biimprd 156 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (suc 𝑦 ⊆ 𝑎 → 𝑥 ⊆ 𝑎)) |
21 | | nfcv 2223 |
. . . . 5
⊢
Ⅎ𝑥𝐴 |
22 | | nfv 1462 |
. . . . 5
⊢
Ⅎ𝑥 𝐴 ⊆ 𝑎 |
23 | | sseq1 3029 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑎 ↔ 𝐴 ⊆ 𝑎)) |
24 | 23 | biimpd 142 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑎 → 𝐴 ⊆ 𝑎)) |
25 | 11, 12, 13, 14, 16, 18, 20, 21, 22, 24 | bj-bdfindisg 11028 |
. . . 4
⊢ ((∅
⊆ 𝑎 ∧
∀𝑦 ∈ ω
(𝑦 ⊆ 𝑎 → suc 𝑦 ⊆ 𝑎)) → (𝐴 ∈ ω → 𝐴 ⊆ 𝑎)) |
26 | 9, 25 | mpan 415 |
. . 3
⊢
(∀𝑦 ∈
ω (𝑦 ⊆ 𝑎 → suc 𝑦 ⊆ 𝑎) → (𝐴 ∈ ω → 𝐴 ⊆ 𝑎)) |
27 | 1, 8, 26 | vtocl 2662 |
. 2
⊢
(∀𝑦 ∈
ω (𝑦 ⊆ ω
→ suc 𝑦 ⊆
ω) → (𝐴 ∈
ω → 𝐴 ⊆
ω)) |
28 | | df-suc 4154 |
. . . 4
⊢ suc 𝑦 = (𝑦 ∪ {𝑦}) |
29 | | simpr 108 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ 𝑦 ⊆ ω) → 𝑦 ⊆
ω) |
30 | | simpl 107 |
. . . . . 6
⊢ ((𝑦 ∈ ω ∧ 𝑦 ⊆ ω) → 𝑦 ∈
ω) |
31 | 30 | snssd 3550 |
. . . . 5
⊢ ((𝑦 ∈ ω ∧ 𝑦 ⊆ ω) → {𝑦} ⊆
ω) |
32 | 29, 31 | unssd 3158 |
. . . 4
⊢ ((𝑦 ∈ ω ∧ 𝑦 ⊆ ω) → (𝑦 ∪ {𝑦}) ⊆ ω) |
33 | 28, 32 | syl5eqss 3052 |
. . 3
⊢ ((𝑦 ∈ ω ∧ 𝑦 ⊆ ω) → suc
𝑦 ⊆
ω) |
34 | 33 | ex 113 |
. 2
⊢ (𝑦 ∈ ω → (𝑦 ⊆ ω → suc
𝑦 ⊆
ω)) |
35 | 27, 34 | mprg 2425 |
1
⊢ (𝐴 ∈ ω → 𝐴 ⊆
ω) |