Step | Hyp | Ref
| Expression |
1 | | limelon 5705 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
2 | | 0ellim 5704 |
. . . . . . 7
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
3 | 2 | adantl 481 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵) |
4 | | oe0m1 7488 |
. . . . . . 7
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
5 | 4 | biimpa 500 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) = ∅) |
6 | 1, 3, 5 | syl2anc 691 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (∅ ↑𝑜
𝐵) =
∅) |
7 | | eldif 3550 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ 1𝑜) ↔
(𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈
1𝑜)) |
8 | | limord 5701 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → Ord 𝐵) |
9 | | ordelon 5664 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
10 | 8, 9 | sylan 487 |
. . . . . . . . . . 11
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
11 | | on0eln0 5697 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ 𝑥 ≠ ∅)) |
12 | | el1o 7466 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 1𝑜
↔ 𝑥 =
∅) |
13 | 12 | necon3bbii 2829 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈
1𝑜 ↔ 𝑥 ≠ ∅) |
14 | 11, 13 | syl6bbr 277 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ ¬ 𝑥 ∈
1𝑜)) |
15 | | oe0m1 7488 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ (∅
↑𝑜 𝑥) = ∅)) |
16 | 15 | biimpd 218 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 → (∅
↑𝑜 𝑥) = ∅)) |
17 | 14, 16 | sylbird 249 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (¬ 𝑥 ∈ 1𝑜
→ (∅ ↑𝑜 𝑥) = ∅)) |
18 | 10, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 1𝑜 → (∅
↑𝑜 𝑥) = ∅)) |
19 | 18 | impr 647 |
. . . . . . . . 9
⊢ ((Lim
𝐵 ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1𝑜)) →
(∅ ↑𝑜 𝑥) = ∅) |
20 | 7, 19 | sylan2b 491 |
. . . . . . . 8
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ (𝐵 ∖ 1𝑜)) →
(∅ ↑𝑜 𝑥) = ∅) |
21 | 20 | iuneq2dv 4478 |
. . . . . . 7
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅
↑𝑜 𝑥) = ∪ 𝑥 ∈ (𝐵 ∖
1𝑜)∅) |
22 | | df-1o 7447 |
. . . . . . . . . . 11
⊢
1𝑜 = suc ∅ |
23 | | limsuc 6941 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → (∅ ∈
𝐵 ↔ suc ∅ ∈
𝐵)) |
24 | 2, 23 | mpbid 221 |
. . . . . . . . . . 11
⊢ (Lim
𝐵 → suc ∅ ∈
𝐵) |
25 | 22, 24 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (Lim
𝐵 →
1𝑜 ∈ 𝐵) |
26 | | 1on 7454 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
27 | 26 | onirri 5751 |
. . . . . . . . . 10
⊢ ¬
1𝑜 ∈ 1𝑜 |
28 | 25, 27 | jctir 559 |
. . . . . . . . 9
⊢ (Lim
𝐵 →
(1𝑜 ∈ 𝐵 ∧ ¬ 1𝑜 ∈
1𝑜)) |
29 | | eldif 3550 |
. . . . . . . . 9
⊢
(1𝑜 ∈ (𝐵 ∖ 1𝑜) ↔
(1𝑜 ∈ 𝐵 ∧ ¬ 1𝑜 ∈
1𝑜)) |
30 | 28, 29 | sylibr 223 |
. . . . . . . 8
⊢ (Lim
𝐵 →
1𝑜 ∈ (𝐵 ∖
1𝑜)) |
31 | | ne0i 3880 |
. . . . . . . 8
⊢
(1𝑜 ∈ (𝐵 ∖ 1𝑜) →
(𝐵 ∖
1𝑜) ≠ ∅) |
32 | | iunconst 4465 |
. . . . . . . 8
⊢ ((𝐵 ∖ 1𝑜)
≠ ∅ → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)∅ =
∅) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . 7
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)∅ =
∅) |
34 | 21, 33 | eqtrd 2644 |
. . . . . 6
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅
↑𝑜 𝑥) = ∅) |
35 | 34 | adantl 481 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∪
𝑥 ∈ (𝐵 ∖ 1𝑜)(∅
↑𝑜 𝑥) = ∅) |
36 | 6, 35 | eqtr4d 2647 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (∅ ↑𝑜
𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅
↑𝑜 𝑥)) |
37 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
38 | | oveq1 6556 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝑥) = (∅
↑𝑜 𝑥)) |
39 | 38 | iuneq2d 4483 |
. . . . 5
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(∅
↑𝑜 𝑥)) |
40 | 37, 39 | eqeq12d 2625 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥) ↔ (∅
↑𝑜 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1𝑜)(∅
↑𝑜 𝑥))) |
41 | 36, 40 | syl5ibr 235 |
. . 3
⊢ (𝐴 = ∅ → ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥))) |
42 | 41 | impcom 445 |
. 2
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |
43 | | oelim 7501 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦)) |
44 | | limsuc 6941 |
. . . . . . . . . . . . 13
⊢ (Lim
𝐵 → (𝑦 ∈ 𝐵 ↔ suc 𝑦 ∈ 𝐵)) |
45 | 44 | biimpa 500 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ∈ 𝐵) |
46 | | nsuceq0 5722 |
. . . . . . . . . . . . 13
⊢ suc 𝑦 ≠ ∅ |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ≠ ∅) |
48 | | dif1o 7467 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ∈ (𝐵 ∖ 1𝑜) ↔ (suc
𝑦 ∈ 𝐵 ∧ suc 𝑦 ≠ ∅)) |
49 | 45, 47, 48 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ∈ (𝐵 ∖
1𝑜)) |
50 | 49 | ex 449 |
. . . . . . . . . 10
⊢ (Lim
𝐵 → (𝑦 ∈ 𝐵 → suc 𝑦 ∈ (𝐵 ∖
1𝑜))) |
51 | 50 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → suc 𝑦 ∈ (𝐵 ∖
1𝑜))) |
52 | | sssucid 5719 |
. . . . . . . . . . 11
⊢ 𝑦 ⊆ suc 𝑦 |
53 | | ordelon 5664 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
54 | 8, 53 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
55 | | suceloni 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
56 | 54, 55 | jccir 560 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) |
57 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
58 | 57 | 3expa 1257 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ On ∧ suc 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
59 | 58 | ancoms 468 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
60 | 56, 59 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (Lim 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
61 | 60 | anassrs 678 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
62 | | oewordi 7558 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
63 | 61, 62 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
64 | 63 | an32s 842 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
65 | 52, 64 | mpi 20 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦)) |
66 | 65 | ex 449 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
67 | 51, 66 | jcad 554 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → (suc 𝑦 ∈ (𝐵 ∖ 1𝑜) ∧ (𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜 suc
𝑦)))) |
68 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 suc 𝑦)) |
69 | 68 | sseq2d 3596 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 𝑥) ↔ (𝐴 ↑𝑜 𝑦) ⊆ (𝐴 ↑𝑜 suc 𝑦))) |
70 | 69 | rspcev 3282 |
. . . . . . . 8
⊢ ((suc
𝑦 ∈ (𝐵 ∖ 1𝑜) ∧ (𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜 suc
𝑦)) → ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜
𝑥)) |
71 | 67, 70 | syl6 34 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜
𝑥))) |
72 | 71 | ralrimiv 2948 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜
𝑥)) |
73 | | iunss2 4501 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑦) ⊆ (𝐴 ↑𝑜
𝑥) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦) ⊆ ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |
74 | 72, 73 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦) ⊆ ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |
75 | | difss 3699 |
. . . . . . . 8
⊢ (𝐵 ∖ 1𝑜)
⊆ 𝐵 |
76 | | iunss1 4468 |
. . . . . . . 8
⊢ ((𝐵 ∖ 1𝑜)
⊆ 𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥) ⊆ ∪ 𝑥 ∈ 𝐵 (𝐴 ↑𝑜 𝑥)) |
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥) ⊆ ∪ 𝑥 ∈ 𝐵 (𝐴 ↑𝑜 𝑥) |
78 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴 ↑𝑜 𝑥) = (𝐴 ↑𝑜 𝑦)) |
79 | 78 | cbviunv 4495 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ↑𝑜 𝑥) = ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦) |
80 | 77, 79 | sseqtri 3600 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥) ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦) |
81 | 80 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥) ⊆ ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦)) |
82 | 74, 81 | eqssd 3585 |
. . . 4
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |
83 | 82 | adantlrl 752 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ∪
𝑦 ∈ 𝐵 (𝐴 ↑𝑜 𝑦) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |
84 | 43, 83 | eqtrd 2644 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |
85 | 42, 84 | oe0lem 7480 |
1
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ↑𝑜 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1𝑜)(𝐴 ↑𝑜
𝑥)) |