| Step | Hyp | Ref
| Expression |
| 1 | | limelon 6448 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → 𝐵 ∈ On) |
| 2 | | 0ellim 6447 |
. . . . . . 7
⊢ (Lim
𝐵 → ∅ ∈
𝐵) |
| 3 | 2 | adantl 481 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∅ ∈ 𝐵) |
| 4 | | oe0m1 8559 |
. . . . . . 7
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
| 5 | 4 | biimpa 476 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑o 𝐵) =
∅) |
| 6 | 1, 3, 5 | syl2anc 584 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (∅ ↑o 𝐵) = ∅) |
| 7 | | eldif 3961 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ 1o) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o)) |
| 8 | | limord 6444 |
. . . . . . . . . . . 12
⊢ (Lim
𝐵 → Ord 𝐵) |
| 9 | | ordelon 6408 |
. . . . . . . . . . . 12
⊢ ((Ord
𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 10 | 8, 9 | sylan 580 |
. . . . . . . . . . 11
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 11 | | on0eln0 6440 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ 𝑥 ≠ ∅)) |
| 12 | | el1o 8533 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 1o ↔
𝑥 =
∅) |
| 13 | 12 | necon3bbii 2988 |
. . . . . . . . . . . . 13
⊢ (¬
𝑥 ∈ 1o
↔ 𝑥 ≠
∅) |
| 14 | 11, 13 | bitr4di 289 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ ¬ 𝑥 ∈
1o)) |
| 15 | | oe0m1 8559 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 ↔ (∅
↑o 𝑥) =
∅)) |
| 16 | 15 | biimpd 229 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → (∅
∈ 𝑥 → (∅
↑o 𝑥) =
∅)) |
| 17 | 14, 16 | sylbird 260 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ On → (¬ 𝑥 ∈ 1o →
(∅ ↑o 𝑥) = ∅)) |
| 18 | 10, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ 1o → (∅
↑o 𝑥) =
∅)) |
| 19 | 18 | impr 454 |
. . . . . . . . 9
⊢ ((Lim
𝐵 ∧ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o)) → (∅
↑o 𝑥) =
∅) |
| 20 | 7, 19 | sylan2b 594 |
. . . . . . . 8
⊢ ((Lim
𝐵 ∧ 𝑥 ∈ (𝐵 ∖ 1o)) → (∅
↑o 𝑥) =
∅) |
| 21 | 20 | iuneq2dv 5016 |
. . . . . . 7
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥) =
∪ 𝑥 ∈ (𝐵 ∖
1o)∅) |
| 22 | | df-1o 8506 |
. . . . . . . . . 10
⊢
1o = suc ∅ |
| 23 | | limsuc 7870 |
. . . . . . . . . . 11
⊢ (Lim
𝐵 → (∅ ∈
𝐵 ↔ suc ∅ ∈
𝐵)) |
| 24 | 2, 23 | mpbid 232 |
. . . . . . . . . 10
⊢ (Lim
𝐵 → suc ∅ ∈
𝐵) |
| 25 | 22, 24 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (Lim
𝐵 → 1o
∈ 𝐵) |
| 26 | | 1on 8518 |
. . . . . . . . . 10
⊢
1o ∈ On |
| 27 | 26 | onirri 6497 |
. . . . . . . . 9
⊢ ¬
1o ∈ 1o |
| 28 | | eldif 3961 |
. . . . . . . . 9
⊢
(1o ∈ (𝐵 ∖ 1o) ↔
(1o ∈ 𝐵
∧ ¬ 1o ∈ 1o)) |
| 29 | 25, 27, 28 | sylanblrc 590 |
. . . . . . . 8
⊢ (Lim
𝐵 → 1o
∈ (𝐵 ∖
1o)) |
| 30 | | ne0i 4341 |
. . . . . . . 8
⊢
(1o ∈ (𝐵 ∖ 1o) → (𝐵 ∖ 1o) ≠
∅) |
| 31 | | iunconst 5001 |
. . . . . . . 8
⊢ ((𝐵 ∖ 1o) ≠
∅ → ∪ 𝑥 ∈ (𝐵 ∖ 1o)∅ =
∅) |
| 32 | 29, 30, 31 | 3syl 18 |
. . . . . . 7
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)∅ =
∅) |
| 33 | 21, 32 | eqtrd 2777 |
. . . . . 6
⊢ (Lim
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥) =
∅) |
| 34 | 33 | adantl 481 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → ∪
𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥) =
∅) |
| 35 | 6, 34 | eqtr4d 2780 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (∅ ↑o 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥)) |
| 36 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
| 37 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝑥) = (∅ ↑o
𝑥)) |
| 38 | 37 | iuneq2d 5022 |
. . . . 5
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥)) |
| 39 | 36, 38 | eqeq12d 2753 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ↔ (∅ ↑o 𝐵) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(∅
↑o 𝑥))) |
| 40 | 35, 39 | imbitrrid 246 |
. . 3
⊢ (𝐴 = ∅ → ((𝐵 ∈ 𝐶 ∧ Lim 𝐵) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥))) |
| 41 | 40 | impcom 407 |
. 2
⊢ (((𝐵 ∈ 𝐶 ∧ Lim 𝐵) ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
| 42 | | oelim 8572 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦)) |
| 43 | | limsuc 7870 |
. . . . . . . . . . . . 13
⊢ (Lim
𝐵 → (𝑦 ∈ 𝐵 ↔ suc 𝑦 ∈ 𝐵)) |
| 44 | 43 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ∈ 𝐵) |
| 45 | | nsuceq0 6467 |
. . . . . . . . . . . 12
⊢ suc 𝑦 ≠ ∅ |
| 46 | | dif1o 8538 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ∈ (𝐵 ∖ 1o) ↔ (suc 𝑦 ∈ 𝐵 ∧ suc 𝑦 ≠ ∅)) |
| 47 | 44, 45, 46 | sylanblrc 590 |
. . . . . . . . . . 11
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → suc 𝑦 ∈ (𝐵 ∖ 1o)) |
| 48 | 47 | ex 412 |
. . . . . . . . . 10
⊢ (Lim
𝐵 → (𝑦 ∈ 𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1o))) |
| 49 | 48 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → suc 𝑦 ∈ (𝐵 ∖ 1o))) |
| 50 | | sssucid 6464 |
. . . . . . . . . . 11
⊢ 𝑦 ⊆ suc 𝑦 |
| 51 | | ordelon 6408 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
| 52 | 8, 51 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ On) |
| 53 | | onsuc 7831 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ On → suc 𝑦 ∈ On) |
| 54 | 52, 53 | jccir 521 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) |
| 55 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
| 56 | 55 | 3expa 1119 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ On ∧ suc 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
| 57 | 56 | ancoms 458 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ (𝑦 ∈ On ∧ suc 𝑦 ∈ On)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
| 58 | 54, 57 | sylan2 593 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ On ∧ (Lim 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
| 59 | 58 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On)) |
| 60 | | oewordi 8629 |
. . . . . . . . . . . . 13
⊢ (((𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
| 61 | 59, 60 | sylan 580 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
| 62 | 61 | an32s 652 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ⊆ suc 𝑦 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
| 63 | 50, 62 | mpi 20 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦)) |
| 64 | 63 | ex 412 |
. . . . . . . . 9
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
| 65 | 49, 64 | jcad 512 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → (suc 𝑦 ∈ (𝐵 ∖ 1o) ∧ (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦)))) |
| 66 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o suc 𝑦)) |
| 67 | 66 | sseq2d 4016 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥) ↔ (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦))) |
| 68 | 67 | rspcev 3622 |
. . . . . . . 8
⊢ ((suc
𝑦 ∈ (𝐵 ∖ 1o) ∧ (𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o suc 𝑦)) → ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥)) |
| 69 | 65, 68 | syl6 35 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥))) |
| 70 | 69 | ralrimiv 3145 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥)) |
| 71 | | iunss2 5049 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑦) ⊆ (𝐴 ↑o 𝑥) → ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) ⊆ ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
| 72 | 70, 71 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) ⊆ ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
| 73 | | difss 4136 |
. . . . . . . 8
⊢ (𝐵 ∖ 1o) ⊆
𝐵 |
| 74 | | iunss1 5006 |
. . . . . . . 8
⊢ ((𝐵 ∖ 1o) ⊆
𝐵 → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥)) |
| 75 | 73, 74 | ax-mp 5 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥) |
| 76 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝐴 ↑o 𝑥) = (𝐴 ↑o 𝑦)) |
| 77 | 76 | cbviunv 5040 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ↑o 𝑥) = ∪ 𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) |
| 78 | 75, 77 | sseqtri 4032 |
. . . . . 6
⊢ ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) |
| 79 | 78 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥) ⊆ ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦)) |
| 80 | 72, 79 | eqssd 4001 |
. . . 4
⊢ (((𝐴 ∈ On ∧ Lim 𝐵) ∧ ∅ ∈ 𝐴) → ∪ 𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
| 81 | 80 | adantlrl 720 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → ∪
𝑦 ∈ 𝐵 (𝐴 ↑o 𝑦) = ∪ 𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
| 82 | 42, 81 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |
| 83 | 41, 82 | oe0lem 8551 |
1
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ 𝐶 ∧ Lim 𝐵)) → (𝐴 ↑o 𝐵) = ∪
𝑥 ∈ (𝐵 ∖ 1o)(𝐴 ↑o 𝑥)) |