| Step | Hyp | Ref
| Expression |
| 1 | | limeq 6396 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (Lim 𝑥 ↔ Lim 𝑧)) |
| 2 | 1 | rspcv 3618 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Lim 𝑥 → Lim 𝑧)) |
| 3 | | vex 3484 |
. . . . . . 7
⊢ 𝑧 ∈ V |
| 4 | | limelon 6448 |
. . . . . . 7
⊢ ((𝑧 ∈ V ∧ Lim 𝑧) → 𝑧 ∈ On) |
| 5 | 3, 4 | mpan 690 |
. . . . . 6
⊢ (Lim
𝑧 → 𝑧 ∈ On) |
| 6 | 2, 5 | syl6com 37 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑧 ∈ 𝐴 → 𝑧 ∈ On)) |
| 7 | 6 | ssrdv 3989 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → 𝐴 ⊆ On) |
| 8 | | ssorduni 7799 |
. . . 4
⊢ (𝐴 ⊆ On → Ord ∪ 𝐴) |
| 9 | 7, 8 | syl 17 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → Ord ∪
𝐴) |
| 10 | 9 | adantl 481 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → Ord ∪
𝐴) |
| 11 | | n0 4353 |
. . . 4
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
| 12 | | 0ellim 6447 |
. . . . . . 7
⊢ (Lim
𝑧 → ∅ ∈
𝑧) |
| 13 | | elunii 4912 |
. . . . . . . 8
⊢ ((∅
∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∅ ∈ ∪ 𝐴) |
| 14 | 13 | expcom 413 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (∅ ∈ 𝑧 → ∅ ∈ ∪ 𝐴)) |
| 15 | 12, 14 | syl5 34 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → (Lim 𝑧 → ∅ ∈ ∪ 𝐴)) |
| 16 | 2, 15 | syld 47 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴)) |
| 17 | 16 | exlimiv 1930 |
. . . 4
⊢
(∃𝑧 𝑧 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴)) |
| 18 | 11, 17 | sylbi 217 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 Lim 𝑥 → ∅ ∈ ∪ 𝐴)) |
| 19 | 18 | imp 406 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → ∅ ∈ ∪ 𝐴) |
| 20 | | eluni2 4911 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝐴
↔ ∃𝑧 ∈
𝐴 𝑦 ∈ 𝑧) |
| 21 | 1 | rspccv 3619 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑧 ∈ 𝐴 → Lim 𝑧)) |
| 22 | | limsuc 7870 |
. . . . . . . . . . 11
⊢ (Lim
𝑧 → (𝑦 ∈ 𝑧 ↔ suc 𝑦 ∈ 𝑧)) |
| 23 | 22 | anbi1d 631 |
. . . . . . . . . 10
⊢ (Lim
𝑧 → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) ↔ (suc 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴))) |
| 24 | | elunii 4912 |
. . . . . . . . . 10
⊢ ((suc
𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → suc 𝑦 ∈ ∪ 𝐴) |
| 25 | 23, 24 | biimtrdi 253 |
. . . . . . . . 9
⊢ (Lim
𝑧 → ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → suc 𝑦 ∈ ∪ 𝐴)) |
| 26 | 25 | expd 415 |
. . . . . . . 8
⊢ (Lim
𝑧 → (𝑦 ∈ 𝑧 → (𝑧 ∈ 𝐴 → suc 𝑦 ∈ ∪ 𝐴))) |
| 27 | 26 | com3r 87 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐴 → (Lim 𝑧 → (𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴))) |
| 28 | 21, 27 | sylcom 30 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑧 ∈ 𝐴 → (𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴))) |
| 29 | 28 | rexlimdv 3153 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 → suc 𝑦 ∈ ∪ 𝐴)) |
| 30 | 20, 29 | biimtrid 242 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → (𝑦 ∈ ∪ 𝐴 → suc 𝑦 ∈ ∪ 𝐴)) |
| 31 | 30 | ralrimiv 3145 |
. . 3
⊢
(∀𝑥 ∈
𝐴 Lim 𝑥 → ∀𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴) |
| 32 | 31 | adantl 481 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → ∀𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴) |
| 33 | | dflim4 7869 |
. 2
⊢ (Lim
∪ 𝐴 ↔ (Ord ∪
𝐴 ∧ ∅ ∈
∪ 𝐴 ∧ ∀𝑦 ∈ ∪ 𝐴 suc 𝑦 ∈ ∪ 𝐴)) |
| 34 | 10, 19, 32, 33 | syl3anbrc 1344 |
1
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 Lim 𝑥) → Lim ∪
𝐴) |