Step | Hyp | Ref
| Expression |
1 | | limelon 6030 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
2 | | 0ellim 6029 |
. . . . . . 7
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
3 | 2 | adantl 475 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵) |
4 | | oe0m1 7873 |
. . . . . . 7
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
5 | 4 | biimpa 470 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑o 𝐵) =
∅) |
6 | 1, 3, 5 | syl2anc 579 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (∅ ↑o 𝐵) = ∅) |
7 | | eldif 3808 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ 1o) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o)) |
8 | | limord 6026 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → Ord 𝐵) |
9 | | ordelon 5991 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
10 | 8, 9 | sylan 575 |
. . . . . . . . . . 11
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
11 | | on0eln0 6022 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ 𝑥 ≠ ∅)) |
12 | | el1o 7851 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 1o ↔
𝑥 =
∅) |
13 | 12 | necon3bbii 3046 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 1o
↔ 𝑥 ≠
∅) |
14 | 11, 13 | syl6bbr 281 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ ¬ 𝑥 ∈
1o)) |
15 | | oe0m1 7873 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ (∅
↑o 𝑥) =
∅)) |
16 | 15 | biimpd 221 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 → (∅
↑o 𝑥) =
∅)) |
17 | 14, 16 | sylbird 252 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (¬ 𝑥 ∈ 1o →
(∅ ↑o 𝑥) = ∅)) |
18 | 10, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 1o → (∅
↑o 𝑥) =
∅)) |
19 | 18 | impr 448 |
. . . . . . . . 9
⊢ ((Lim
𝐵 ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o)) → (∅
↑o 𝑥) =
∅) |
20 | 7, 19 | sylan2b 587 |
. . . . . . . 8
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ (𝐵 ∖ 1o)) → (∅
↑o 𝑥) =
∅) |
21 | 20 | iuneq2dv 4764 |
. . . . . . 7
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥) =
∪ 𝑥 ∈ (𝐵 ∖
1o)∅) |
22 | | df-1o 7831 |
. . . . . . . . . . 11
⊢
1o = suc ∅ |
23 | | limsuc 7315 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → (∅ ∈
𝐵 ↔ suc ∅ ∈
𝐵)) |
24 | 2, 23 | mpbid 224 |
. . . . . . . . . . 11
⊢ (Lim
𝐵 → suc ∅ ∈
𝐵) |
25 | 22, 24 | syl5eqel 2910 |
. . . . . . . . . 10
⊢ (Lim
𝐵 → 1o
∈ 𝐵) |
26 | | 1on 7838 |
. . . . . . . . . . 11
⊢
1o ∈ On |
27 | 26 | onirri 6073 |
. . . . . . . . . 10
⊢ ¬
1o ∈ 1o |
28 | 25, 27 | jctir 516 |
. . . . . . . . 9
⊢ (Lim
𝐵 → (1o
∈ 𝐵 ∧ ¬
1o ∈ 1o)) |
29 | | eldif 3808 |
. . . . . . . . 9
⊢
(1o ∈ (𝐵 ∖ 1o) ↔
(1o ∈ 𝐵
∧ ¬ 1o ∈ 1o)) |
30 | 28, 29 | sylibr 226 |
. . . . . . . 8
⊢ (Lim
𝐵 → 1o
∈ (𝐵 ∖
1o)) |
31 | | ne0i 4152 |
. . . . . . . 8
⊢
(1o ∈ (𝐵 ∖ 1o) → (𝐵 ∖ 1o) ≠
∅) |
32 | | iunconst 4751 |
. . . . . . . 8
⊢ ((𝐵 ∖ 1o) ≠
∅ → ∪ 𝑥 ∈ (𝐵 ∖ 1o)∅ =
∅) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . 7
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)∅ =
∅) |
34 | 21, 33 | eqtrd 2861 |
. . . . . 6
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥) =
∅) |
35 | 34 | adantl 475 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∪
𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥) =
∅) |
36 | 6, 35 | eqtr4d 2864 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (∅ ↑o 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥)) |
37 | | oveq1 6917 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
38 | | oveq1 6917 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝑥) = (∅ ↑o
𝑥)) |
39 | 38 | iuneq2d 4769 |
. . . . 5
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥)) |
40 | 37, 39 | eqeq12d 2840 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ↔ (∅ ↑o 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥))) |
41 | 36, 40 | syl5ibr 238 |
. . 3
⊢ (𝐴 = ∅ → ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥))) |
42 | 41 | impcom 398 |
. 2
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
43 | | oelim 7886 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦)) |
44 | | limsuc 7315 |
. . . . . . . . . . . . 13
⊢ (Lim
𝐵 → (𝑦 ∈ 𝐵 ↔ suc 𝑦 ∈ 𝐵)) |
45 | 44 | biimpa 470 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ∈ 𝐵) |
46 | | nsuceq0 6047 |
. . . . . . . . . . . . 13
⊢ suc 𝑦 ≠ ∅ |
47 | 46 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ≠ ∅) |
48 | | dif1o 7852 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ∈ (𝐵 ∖ 1o) ↔ (suc 𝑦 ∈ 𝐵 ∧ suc 𝑦 ≠ ∅)) |
49 | 45, 47, 48 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ∈ (𝐵 ∖ 1o)) |
50 | 49 | ex 403 |
. . . . . . . . . 10
⊢ (Lim
𝐵 → (𝑦 ∈ 𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1o))) |
51 | 50 | ad2antlr 718 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1o))) |
52 | | sssucid 6044 |
. . . . . . . . . . 11
⊢ 𝑦 ⊆ suc 𝑦 |
53 | | ordelon 5991 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
54 | 8, 53 | sylan 575 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
55 | | suceloni 7279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
56 | 54, 55 | jccir 517 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) |
57 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
58 | 57 | 3expa 1151 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ On ∧ suc 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
59 | 58 | ancoms 452 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
60 | 56, 59 | sylan2 586 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (Lim 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
61 | 60 | anassrs 461 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
62 | | oewordi 7943 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
63 | 61, 62 | sylan 575 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
64 | 63 | an32s 642 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
65 | 52, 64 | mpi 20 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦)) |
66 | 65 | ex 403 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
67 | 51, 66 | jcad 508 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → (suc 𝑦 ∈ (𝐵 ∖ 1o) ∧ (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦)))) |
68 | | oveq2 6918 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝑦)) |
69 | 68 | sseq2d 3858 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥) ↔ (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
70 | 69 | rspcev 3526 |
. . . . . . . 8
⊢ ((suc
𝑦 ∈ (𝐵 ∖ 1o) ∧ (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦)) → ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥)) |
71 | 67, 70 | syl6 35 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥))) |
72 | 71 | ralrimiv 3174 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥)) |
73 | | iunss2 4787 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥) → ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) ⊆ ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
74 | 72, 73 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) ⊆ ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
75 | | difss 3966 |
. . . . . . . 8
⊢ (𝐵 ∖ 1o) ⊆
𝐵 |
76 | | iunss1 4754 |
. . . . . . . 8
⊢ ((𝐵 ∖ 1o) ⊆
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥)) |
77 | 75, 76 | ax-mp 5 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥) |
78 | | oveq2 6918 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
79 | 78 | cbviunv 4781 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) |
80 | 77, 79 | sseqtri 3862 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) |
81 | 80 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦)) |
82 | 74, 81 | eqssd 3844 |
. . . 4
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
83 | 82 | adantlrl 711 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
84 | 43, 83 | eqtrd 2861 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
85 | 42, 84 | oe0lem 7865 |
1
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |