Proof of Theorem omlimcl2
Step | Hyp | Ref
| Expression |
1 | | eloni 6326 |
. . . . . 6
⊢ (𝐴 ∈ On → Ord 𝐴) |
2 | 1 | ad2antrr 724 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Ord 𝐴) |
3 | | ne0i 4293 |
. . . . . 6
⊢ (∅
∈ 𝐴 → 𝐴 ≠ ∅) |
4 | 3 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → 𝐴 ≠ ∅) |
5 | | id 22 |
. . . . 5
⊢ (𝐴 = ∪
𝐴 → 𝐴 = ∪ 𝐴) |
6 | | df-lim 6321 |
. . . . . 6
⊢ (Lim
𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) |
7 | 6 | biimpri 227 |
. . . . 5
⊢ ((Ord
𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) → Lim 𝐴) |
8 | 2, 4, 5, 7 | syl2an3an 1422 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = ∪ 𝐴) → Lim 𝐴) |
9 | 8 | ex 413 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 = ∪ 𝐴 → Lim 𝐴)) |
10 | | limelon 6380 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
11 | 10 | ad3antlr 729 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝐴) → 𝐵 ∈ On) |
12 | | simpll 765 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → 𝐴 ∈ On) |
13 | 12 | anim1i 615 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝐴) → (𝐴 ∈ On ∧ Lim 𝐴)) |
14 | | 0ellim 6379 |
. . . . . . 7
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
15 | 14 | adantl 482 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵) |
16 | 15 | ad3antlr 729 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝐴) → ∅ ∈ 𝐵) |
17 | | omlimcl 8522 |
. . . . 5
⊢ (((𝐵 ∈ On ∧ (𝐴 ∈ On ∧ Lim 𝐴)) ∧ ∅ ∈ 𝐵) → Lim (𝐵 ·o 𝐴)) |
18 | 11, 13, 16, 17 | syl21anc 836 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ Lim 𝐴) → Lim (𝐵 ·o 𝐴)) |
19 | 18 | ex 413 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (Lim 𝐴 → Lim (𝐵 ·o 𝐴))) |
20 | 9, 19 | syld 47 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 = ∪ 𝐴 → Lim (𝐵 ·o 𝐴))) |
21 | | onuni 7720 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ∪ 𝐴
∈ On) |
22 | 21, 10 | anim12ci 614 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐵 ∈ On ∧ ∪ 𝐴
∈ On)) |
23 | | omcl 8479 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ ∪ 𝐴
∈ On) → (𝐵
·o ∪ 𝐴) ∈ On) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐵 ·o ∪ 𝐴)
∈ On) |
25 | | simpr 485 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) |
26 | 24, 25 | jca 512 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → ((𝐵 ·o ∪ 𝐴)
∈ On ∧ (𝐵 ∈
𝐶 ∧ Lim 𝐵))) |
27 | 26 | ad2antrr 724 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → ((𝐵 ·o ∪ 𝐴)
∈ On ∧ (𝐵 ∈
𝐶 ∧ Lim 𝐵))) |
28 | | oalimcl 8504 |
. . . . 5
⊢ (((𝐵 ·o ∪ 𝐴)
∈ On ∧ (𝐵 ∈
𝐶 ∧ Lim 𝐵)) → Lim ((𝐵 ·o ∪ 𝐴)
+o 𝐵)) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → Lim ((𝐵 ·o ∪ 𝐴)
+o 𝐵)) |
30 | | simpr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → 𝐴 = suc ∪ 𝐴) |
31 | 30 | oveq2d 7370 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → (𝐵 ·o 𝐴) = (𝐵 ·o suc ∪ 𝐴)) |
32 | 22 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → (𝐵 ∈ On ∧ ∪ 𝐴
∈ On)) |
33 | | omsuc 8469 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ ∪ 𝐴
∈ On) → (𝐵
·o suc ∪ 𝐴) = ((𝐵 ·o ∪ 𝐴)
+o 𝐵)) |
34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → (𝐵 ·o suc ∪ 𝐴) =
((𝐵 ·o
∪ 𝐴) +o 𝐵)) |
35 | 31, 34 | eqtrd 2776 |
. . . . 5
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → (𝐵 ·o 𝐴) = ((𝐵 ·o ∪ 𝐴)
+o 𝐵)) |
36 | | limeq 6328 |
. . . . 5
⊢ ((𝐵 ·o 𝐴) = ((𝐵 ·o ∪ 𝐴)
+o 𝐵) →
(Lim (𝐵
·o 𝐴)
↔ Lim ((𝐵
·o ∪ 𝐴) +o 𝐵))) |
37 | 35, 36 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → (Lim (𝐵 ·o 𝐴) ↔ Lim ((𝐵 ·o ∪ 𝐴)
+o 𝐵))) |
38 | 29, 37 | mpbird 256 |
. . 3
⊢ ((((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) ∧ 𝐴 = suc ∪ 𝐴) → Lim (𝐵 ·o 𝐴)) |
39 | 38 | ex 413 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 = suc ∪ 𝐴 → Lim (𝐵 ·o 𝐴))) |
40 | | orduniorsuc 7762 |
. . 3
⊢ (Ord
𝐴 → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) |
41 | 2, 40 | syl 17 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴)) |
42 | 20, 39, 41 | mpjaod 858 |
1
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → Lim (𝐵 ·o 𝐴)) |