Step | Hyp | Ref
| Expression |
1 | | limeq 6277 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (Lim 𝑥 ↔ Lim 𝑧)) |
2 | 1 | rspcv 3556 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Lim 𝑥 → Lim 𝑧)) |
3 | | vex 3435 |
. . . . . . 7
⊢ 𝑧 ∈ V |
4 | | limelon 6328 |
. . . . . . 7
⊢ ((𝑧 ∈ V ∧ Lim 𝑧) → 𝑧 ∈ On) |
5 | 3, 4 | mpan 687 |
. . . . . 6
⊢ (Lim
𝑧 → 𝑧 ∈ On) |
6 | 2, 5 | syl6com 37 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑧 ∈ 𝐴 → 𝑧 ∈ On)) |
7 | 6 | ssrdv 3932 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → 𝐴 ⊆ On) |
8 | | ssorduni 7623 |
. . . 4
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
9 | 7, 8 | syl 17 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → Ord ∪
𝐴) |
10 | 9 | adantl 482 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → Ord ∪
𝐴) |
11 | | n0 4286 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
12 | | 0ellim 6327 |
. . . . . . 7
⊢ (Lim
𝑧 → ∅ ∈
𝑧) |
13 | | elunii 4850 |
. . . . . . . 8
⊢ ((∅
∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∅ ∈ ∪ 𝐴) |
14 | 13 | expcom 414 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (∅ ∈ 𝑧 → ∅ ∈ ∪ 𝐴)) |
15 | 12, 14 | syl5 34 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → (Lim 𝑧 → ∅ ∈ ∪ 𝐴)) |
16 | 2, 15 | syld 47 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴)) |
17 | 16 | exlimiv 1937 |
. . . 4
⊢
(∃𝑧 𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴)) |
18 | 11, 17 | sylbi 216 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴)) |
19 | 18 | imp 407 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → ∅ ∈ ∪ 𝐴) |
20 | | eluni2 4849 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑧 ∈
𝐴 𝑦 ∈ 𝑧) |
21 | 1 | rspccv 3558 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑧 ∈ 𝐴 → Lim 𝑧)) |
22 | | limsuc 7690 |
. . . . . . . . . . 11
⊢ (Lim
𝑧 → (𝑦 ∈ 𝑧 ↔ suc 𝑦 ∈ 𝑧)) |
23 | 22 | anbi1d 630 |
. . . . . . . . . 10
⊢ (Lim
𝑧 → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) ↔ (suc 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴))) |
24 | | elunii 4850 |
. . . . . . . . . 10
⊢ ((suc
𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → suc 𝑦 ∈ ∪ 𝐴) |
25 | 23, 24 | syl6bi 252 |
. . . . . . . . 9
⊢ (Lim
𝑧 → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → suc 𝑦 ∈ ∪ 𝐴)) |
26 | 25 | expd 416 |
. . . . . . . 8
⊢ (Lim
𝑧 → (𝑦 ∈ 𝑧 → (𝑧 ∈ 𝐴 → suc 𝑦 ∈ ∪ 𝐴))) |
27 | 26 | com3r 87 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (Lim 𝑧 → (𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴))) |
28 | 21, 27 | sylcom 30 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑧 ∈ 𝐴 → (𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴))) |
29 | 28 | rexlimdv 3214 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴)) |
30 | 20, 29 | syl5bi 241 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑦 ∈ ∪ 𝐴 → suc 𝑦 ∈ ∪ 𝐴)) |
31 | 30 | ralrimiv 3109 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → ∀𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴) |
32 | 31 | adantl 482 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → ∀𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴) |
33 | | dflim4 7689 |
. 2
⊢ (Lim
∪ 𝐴 ↔ (Ord ∪
𝐴 ∧ ∅ ∈
∪ 𝐴 ∧ ∀𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴)) |
34 | 10, 19, 32, 33 | syl3anbrc 1342 |
1
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → Lim ∪
𝐴) |