| Step | Hyp | Ref
| Expression |
| 1 | | suceq 6450 |
. . . . 5
⊢ (𝑛 = ∅ → suc 𝑛 = suc ∅) |
| 2 | 1 | raleqdv 3326 |
. . . 4
⊢ (𝑛 = ∅ → (∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 ↔ ∀𝑘 ∈ suc ∅(𝐵‘𝑘) ≈ 𝒫 𝑘)) |
| 3 | | iuneq1 5008 |
. . . . 5
⊢ (𝑛 = ∅ → ∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) = ∪ 𝑘 ∈ ∅ (𝐵‘𝑘)) |
| 4 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = ∅ → (𝐵‘𝑛) = (𝐵‘∅)) |
| 5 | 3, 4 | breq12d 5156 |
. . . 4
⊢ (𝑛 = ∅ → (∪ 𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛) ↔ ∪
𝑘 ∈ ∅ (𝐵‘𝑘) ≺ (𝐵‘∅))) |
| 6 | 2, 5 | imbi12d 344 |
. . 3
⊢ (𝑛 = ∅ →
((∀𝑘 ∈ suc
𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) ↔ (∀𝑘 ∈ suc ∅(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ ∅ (𝐵‘𝑘) ≺ (𝐵‘∅)))) |
| 7 | | suceq 6450 |
. . . . 5
⊢ (𝑛 = 𝑚 → suc 𝑛 = suc 𝑚) |
| 8 | 7 | raleqdv 3326 |
. . . 4
⊢ (𝑛 = 𝑚 → (∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 ↔ ∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘)) |
| 9 | | iuneq1 5008 |
. . . . 5
⊢ (𝑛 = 𝑚 → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) = ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) |
| 10 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝐵‘𝑛) = (𝐵‘𝑚)) |
| 11 | 9, 10 | breq12d 5156 |
. . . 4
⊢ (𝑛 = 𝑚 → (∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛) ↔ ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚))) |
| 12 | 8, 11 | imbi12d 344 |
. . 3
⊢ (𝑛 = 𝑚 → ((∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) ↔ (∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)))) |
| 13 | | suceq 6450 |
. . . . 5
⊢ (𝑛 = suc 𝑚 → suc 𝑛 = suc suc 𝑚) |
| 14 | 13 | raleqdv 3326 |
. . . 4
⊢ (𝑛 = suc 𝑚 → (∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 ↔ ∀𝑘 ∈ suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘)) |
| 15 | | iuneq1 5008 |
. . . . 5
⊢ (𝑛 = suc 𝑚 → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) = ∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘)) |
| 16 | | fveq2 6906 |
. . . . 5
⊢ (𝑛 = suc 𝑚 → (𝐵‘𝑛) = (𝐵‘suc 𝑚)) |
| 17 | 15, 16 | breq12d 5156 |
. . . 4
⊢ (𝑛 = suc 𝑚 → (∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛) ↔ ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚))) |
| 18 | 14, 17 | imbi12d 344 |
. . 3
⊢ (𝑛 = suc 𝑚 → ((∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) ↔ (∀𝑘 ∈ suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚)))) |
| 19 | | 0iun 5063 |
. . . 4
⊢ ∪ 𝑘 ∈ ∅ (𝐵‘𝑘) = ∅ |
| 20 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 21 | 20 | sucid 6466 |
. . . . . 6
⊢ ∅
∈ suc ∅ |
| 22 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = ∅ → (𝐵‘𝑘) = (𝐵‘∅)) |
| 23 | | pweq 4614 |
. . . . . . . 8
⊢ (𝑘 = ∅ → 𝒫
𝑘 = 𝒫
∅) |
| 24 | 22, 23 | breq12d 5156 |
. . . . . . 7
⊢ (𝑘 = ∅ → ((𝐵‘𝑘) ≈ 𝒫 𝑘 ↔ (𝐵‘∅) ≈ 𝒫
∅)) |
| 25 | 24 | rspcv 3618 |
. . . . . 6
⊢ (∅
∈ suc ∅ → (∀𝑘 ∈ suc ∅(𝐵‘𝑘) ≈ 𝒫 𝑘 → (𝐵‘∅) ≈ 𝒫
∅)) |
| 26 | 21, 25 | ax-mp 5 |
. . . . 5
⊢
(∀𝑘 ∈
suc ∅(𝐵‘𝑘) ≈ 𝒫 𝑘 → (𝐵‘∅) ≈ 𝒫
∅) |
| 27 | 20 | canth2 9170 |
. . . . . 6
⊢ ∅
≺ 𝒫 ∅ |
| 28 | | ensym 9043 |
. . . . . 6
⊢ ((𝐵‘∅) ≈
𝒫 ∅ → 𝒫 ∅ ≈ (𝐵‘∅)) |
| 29 | | sdomentr 9151 |
. . . . . 6
⊢ ((∅
≺ 𝒫 ∅ ∧ 𝒫 ∅ ≈ (𝐵‘∅)) → ∅ ≺
(𝐵‘∅)) |
| 30 | 27, 28, 29 | sylancr 587 |
. . . . 5
⊢ ((𝐵‘∅) ≈
𝒫 ∅ → ∅ ≺ (𝐵‘∅)) |
| 31 | 26, 30 | syl 17 |
. . . 4
⊢
(∀𝑘 ∈
suc ∅(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∅ ≺ (𝐵‘∅)) |
| 32 | 19, 31 | eqbrtrid 5178 |
. . 3
⊢
(∀𝑘 ∈
suc ∅(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪ 𝑘 ∈ ∅ (𝐵‘𝑘) ≺ (𝐵‘∅)) |
| 33 | | sssucid 6464 |
. . . . . . . . 9
⊢ suc 𝑚 ⊆ suc suc 𝑚 |
| 34 | | ssralv 4052 |
. . . . . . . . 9
⊢ (suc
𝑚 ⊆ suc suc 𝑚 → (∀𝑘 ∈ suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘)) |
| 35 | 33, 34 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) |
| 36 | | pm2.27 42 |
. . . . . . . 8
⊢
(∀𝑘 ∈
suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ((∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚))) |
| 37 | 35, 36 | syl 17 |
. . . . . . 7
⊢
(∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ((∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚))) |
| 38 | 37 | adantl 481 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧
∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) → ((∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚))) |
| 39 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑚 ∈ V |
| 40 | 39 | sucid 6466 |
. . . . . . . . . . . 12
⊢ 𝑚 ∈ suc 𝑚 |
| 41 | | elelsuc 6457 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ suc 𝑚 → 𝑚 ∈ suc suc 𝑚) |
| 42 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (𝐵‘𝑘) = (𝐵‘𝑚)) |
| 43 | | pweq 4614 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → 𝒫 𝑘 = 𝒫 𝑚) |
| 44 | 42, 43 | breq12d 5156 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((𝐵‘𝑘) ≈ 𝒫 𝑘 ↔ (𝐵‘𝑚) ≈ 𝒫 𝑚)) |
| 45 | 44 | rspcv 3618 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ suc suc 𝑚 → (∀𝑘 ∈ suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → (𝐵‘𝑚) ≈ 𝒫 𝑚)) |
| 46 | 40, 41, 45 | mp2b 10 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → (𝐵‘𝑚) ≈ 𝒫 𝑚) |
| 47 | | djuen 10210 |
. . . . . . . . . . 11
⊢ (((𝐵‘𝑚) ≈ 𝒫 𝑚 ∧ (𝐵‘𝑚) ≈ 𝒫 𝑚) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝒫 𝑚 ⊔ 𝒫 𝑚)) |
| 48 | 46, 46, 47 | syl2anc 584 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝒫 𝑚 ⊔ 𝒫 𝑚)) |
| 49 | | pwdju1 10231 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω →
(𝒫 𝑚 ⊔
𝒫 𝑚) ≈
𝒫 (𝑚 ⊔
1o)) |
| 50 | | nnord 7895 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ω → Ord 𝑚) |
| 51 | | ordirr 6402 |
. . . . . . . . . . . . . 14
⊢ (Ord
𝑚 → ¬ 𝑚 ∈ 𝑚) |
| 52 | 50, 51 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ω → ¬
𝑚 ∈ 𝑚) |
| 53 | | dju1en 10212 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ω ∧ ¬
𝑚 ∈ 𝑚) → (𝑚 ⊔ 1o) ≈ suc 𝑚) |
| 54 | 52, 53 | mpdan 687 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ω → (𝑚 ⊔ 1o) ≈
suc 𝑚) |
| 55 | | pwen 9190 |
. . . . . . . . . . . 12
⊢ ((𝑚 ⊔ 1o) ≈
suc 𝑚 → 𝒫
(𝑚 ⊔ 1o)
≈ 𝒫 suc 𝑚) |
| 56 | 54, 55 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω → 𝒫
(𝑚 ⊔ 1o)
≈ 𝒫 suc 𝑚) |
| 57 | | entr 9046 |
. . . . . . . . . . 11
⊢
(((𝒫 𝑚
⊔ 𝒫 𝑚)
≈ 𝒫 (𝑚
⊔ 1o) ∧ 𝒫 (𝑚 ⊔ 1o) ≈ 𝒫
suc 𝑚) → (𝒫
𝑚 ⊔ 𝒫 𝑚) ≈ 𝒫 suc 𝑚) |
| 58 | 49, 56, 57 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ω →
(𝒫 𝑚 ⊔
𝒫 𝑚) ≈
𝒫 suc 𝑚) |
| 59 | | entr 9046 |
. . . . . . . . . 10
⊢ ((((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝒫 𝑚 ⊔ 𝒫 𝑚) ∧ (𝒫 𝑚 ⊔ 𝒫 𝑚) ≈ 𝒫 suc 𝑚) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ 𝒫 suc 𝑚) |
| 60 | 48, 58, 59 | syl2an 596 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 ∧ 𝑚 ∈ ω) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ 𝒫 suc 𝑚) |
| 61 | 39 | sucex 7826 |
. . . . . . . . . . . . 13
⊢ suc 𝑚 ∈ V |
| 62 | 61 | sucid 6466 |
. . . . . . . . . . . 12
⊢ suc 𝑚 ∈ suc suc 𝑚 |
| 63 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = suc 𝑚 → (𝐵‘𝑘) = (𝐵‘suc 𝑚)) |
| 64 | | pweq 4614 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = suc 𝑚 → 𝒫 𝑘 = 𝒫 suc 𝑚) |
| 65 | 63, 64 | breq12d 5156 |
. . . . . . . . . . . . 13
⊢ (𝑘 = suc 𝑚 → ((𝐵‘𝑘) ≈ 𝒫 𝑘 ↔ (𝐵‘suc 𝑚) ≈ 𝒫 suc 𝑚)) |
| 66 | 65 | rspcv 3618 |
. . . . . . . . . . . 12
⊢ (suc
𝑚 ∈ suc suc 𝑚 → (∀𝑘 ∈ suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → (𝐵‘suc 𝑚) ≈ 𝒫 suc 𝑚)) |
| 67 | 62, 66 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → (𝐵‘suc 𝑚) ≈ 𝒫 suc 𝑚) |
| 68 | 67 | ensymd 9045 |
. . . . . . . . . 10
⊢
(∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → 𝒫 suc 𝑚 ≈ (𝐵‘suc 𝑚)) |
| 69 | 68 | adantr 480 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 ∧ 𝑚 ∈ ω) → 𝒫 suc 𝑚 ≈ (𝐵‘suc 𝑚)) |
| 70 | | entr 9046 |
. . . . . . . . 9
⊢ ((((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ 𝒫 suc 𝑚 ∧ 𝒫 suc 𝑚 ≈ (𝐵‘suc 𝑚)) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝐵‘suc 𝑚)) |
| 71 | 60, 69, 70 | syl2anc 584 |
. . . . . . . 8
⊢
((∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 ∧ 𝑚 ∈ ω) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝐵‘suc 𝑚)) |
| 72 | 71 | ancoms 458 |
. . . . . . 7
⊢ ((𝑚 ∈ ω ∧
∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝐵‘suc 𝑚)) |
| 73 | | nnfi 9207 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ω → 𝑚 ∈ Fin) |
| 74 | | pwfi 9357 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ Fin ↔ 𝒫
𝑚 ∈
Fin) |
| 75 | | isfinite 9692 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑚 ∈
Fin ↔ 𝒫 𝑚
≺ ω) |
| 76 | 74, 75 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ Fin ↔ 𝒫
𝑚 ≺
ω) |
| 77 | 73, 76 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ω → 𝒫
𝑚 ≺
ω) |
| 78 | | ensdomtr 9153 |
. . . . . . . . . . 11
⊢ (((𝐵‘𝑚) ≈ 𝒫 𝑚 ∧ 𝒫 𝑚 ≺ ω) → (𝐵‘𝑚) ≺ ω) |
| 79 | 46, 77, 78 | syl2an 596 |
. . . . . . . . . 10
⊢
((∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 ∧ 𝑚 ∈ ω) → (𝐵‘𝑚) ≺ ω) |
| 80 | | isfinite 9692 |
. . . . . . . . . 10
⊢ ((𝐵‘𝑚) ∈ Fin ↔ (𝐵‘𝑚) ≺ ω) |
| 81 | 79, 80 | sylibr 234 |
. . . . . . . . 9
⊢
((∀𝑘 ∈
suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 ∧ 𝑚 ∈ ω) → (𝐵‘𝑚) ∈ Fin) |
| 82 | 81 | ancoms 458 |
. . . . . . . 8
⊢ ((𝑚 ∈ ω ∧
∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) → (𝐵‘𝑚) ∈ Fin) |
| 83 | 39, 42 | iunsuc 6469 |
. . . . . . . . . . 11
⊢ ∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘) = (∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ∪ (𝐵‘𝑚)) |
| 84 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝐵‘𝑘) ∈ V |
| 85 | 39, 84 | iunex 7993 |
. . . . . . . . . . . 12
⊢ ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ V |
| 86 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐵‘𝑚) ∈ V |
| 87 | | undjudom 10208 |
. . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ V ∧ (𝐵‘𝑚) ∈ V) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∪ (𝐵‘𝑚)) ≼ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚))) |
| 88 | 85, 86, 87 | mp2an 692 |
. . . . . . . . . . 11
⊢ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∪ (𝐵‘𝑚)) ≼ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) |
| 89 | 83, 88 | eqbrtri 5164 |
. . . . . . . . . 10
⊢ ∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≼ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) |
| 90 | | sdomtr 9155 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ≺ ω) → ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ ω) |
| 91 | 80, 90 | sylan2b 594 |
. . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ ω) |
| 92 | | isfinite 9692 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ Fin ↔ ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ ω) |
| 93 | 91, 92 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ Fin) |
| 94 | | finnum 9988 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ Fin → ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ dom card) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ dom card) |
| 96 | | finnum 9988 |
. . . . . . . . . . . . . 14
⊢ ((𝐵‘𝑚) ∈ Fin → (𝐵‘𝑚) ∈ dom card) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (𝐵‘𝑚) ∈ dom card) |
| 98 | | cardadju 10235 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ dom card ∧ (𝐵‘𝑚) ∈ dom card) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≈ ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚)))) |
| 99 | 95, 97, 98 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≈ ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚)))) |
| 100 | | ficardom 10001 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ Fin → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ ω) |
| 101 | 93, 100 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ ω) |
| 102 | | ficardom 10001 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘𝑚) ∈ Fin → (card‘(𝐵‘𝑚)) ∈ ω) |
| 103 | 102 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (card‘(𝐵‘𝑚)) ∈ ω) |
| 104 | | cardid2 9993 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∈ dom card → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≈ ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) |
| 105 | 93, 94, 104 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≈ ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) |
| 106 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) |
| 107 | | cardid2 9993 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵‘𝑚) ∈ dom card → (card‘(𝐵‘𝑚)) ≈ (𝐵‘𝑚)) |
| 108 | | ensym 9043 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘(𝐵‘𝑚)) ≈ (𝐵‘𝑚) → (𝐵‘𝑚) ≈ (card‘(𝐵‘𝑚))) |
| 109 | 96, 107, 108 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵‘𝑚) ∈ Fin → (𝐵‘𝑚) ≈ (card‘(𝐵‘𝑚))) |
| 110 | 109 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (𝐵‘𝑚) ≈ (card‘(𝐵‘𝑚))) |
| 111 | | ensdomtr 9153 |
. . . . . . . . . . . . . . . . . 18
⊢
(((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≈ ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∧ ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (𝐵‘𝑚)) |
| 112 | | sdomentr 9151 |
. . . . . . . . . . . . . . . . . 18
⊢
(((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ≈ (card‘(𝐵‘𝑚))) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (card‘(𝐵‘𝑚))) |
| 113 | 111, 112 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢
((((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≈ ∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ∧ ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) ∧ (𝐵‘𝑚) ≈ (card‘(𝐵‘𝑚))) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (card‘(𝐵‘𝑚))) |
| 114 | 105, 106,
110, 113 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (card‘(𝐵‘𝑚))) |
| 115 | | cardon 9984 |
. . . . . . . . . . . . . . . . . 18
⊢
(card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ On |
| 116 | | cardon 9984 |
. . . . . . . . . . . . . . . . . . 19
⊢
(card‘(𝐵‘𝑚)) ∈ On |
| 117 | | onenon 9989 |
. . . . . . . . . . . . . . . . . . 19
⊢
((card‘(𝐵‘𝑚)) ∈ On → (card‘(𝐵‘𝑚)) ∈ dom card) |
| 118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(card‘(𝐵‘𝑚)) ∈ dom card |
| 119 | | cardsdomel 10014 |
. . . . . . . . . . . . . . . . . 18
⊢
(((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ On ∧ (card‘(𝐵‘𝑚)) ∈ dom card) →
((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (card‘(𝐵‘𝑚)) ↔ (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(card‘(𝐵‘𝑚))))) |
| 120 | 115, 118,
119 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (card‘(𝐵‘𝑚)) ↔ (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(card‘(𝐵‘𝑚)))) |
| 121 | | cardidm 9999 |
. . . . . . . . . . . . . . . . . 18
⊢
(card‘(card‘(𝐵‘𝑚))) = (card‘(𝐵‘𝑚)) |
| 122 | 121 | eleq2i 2833 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(card‘(𝐵‘𝑚))) ↔ (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(𝐵‘𝑚))) |
| 123 | 120, 122 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢
((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ≺ (card‘(𝐵‘𝑚)) ↔ (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(𝐵‘𝑚))) |
| 124 | 114, 123 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(𝐵‘𝑚))) |
| 125 | | nnaordr 8658 |
. . . . . . . . . . . . . . . 16
⊢
(((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ ω ∧ (card‘(𝐵‘𝑚)) ∈ ω ∧ (card‘(𝐵‘𝑚)) ∈ ω) →
((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(𝐵‘𝑚)) ↔ ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ∈ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))))) |
| 126 | 125 | biimpa 476 |
. . . . . . . . . . . . . . 15
⊢
((((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ ω ∧ (card‘(𝐵‘𝑚)) ∈ ω ∧ (card‘(𝐵‘𝑚)) ∈ ω) ∧ (card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) ∈ (card‘(𝐵‘𝑚))) → ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ∈ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 127 | 101, 103,
103, 124, 126 | syl31anc 1375 |
. . . . . . . . . . . . . 14
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ∈ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 128 | | nnacl 8649 |
. . . . . . . . . . . . . . . . 17
⊢
(((card‘(𝐵‘𝑚)) ∈ ω ∧ (card‘(𝐵‘𝑚)) ∈ ω) → ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ∈ ω) |
| 129 | 102, 102,
128 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵‘𝑚) ∈ Fin → ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ∈ ω) |
| 130 | | cardnn 10003 |
. . . . . . . . . . . . . . . 16
⊢
(((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ∈ ω →
(card‘((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) = ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 131 | 129, 130 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵‘𝑚) ∈ Fin →
(card‘((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) = ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 132 | 131 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) →
(card‘((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) = ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 133 | 127, 132 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ∈ (card‘((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))))) |
| 134 | | cardsdomelir 10013 |
. . . . . . . . . . . . 13
⊢
(((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ∈ (card‘((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) → ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ≺ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 135 | 133, 134 | syl 17 |
. . . . . . . . . . . 12
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ≺ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 136 | | ensdomtr 9153 |
. . . . . . . . . . . 12
⊢
(((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≈ ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ∧ ((card‘∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘)) +o (card‘(𝐵‘𝑚))) ≺ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≺ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 137 | 99, 135, 136 | syl2anc 584 |
. . . . . . . . . . 11
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≺ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 138 | | cardadju 10235 |
. . . . . . . . . . . . . 14
⊢ (((𝐵‘𝑚) ∈ dom card ∧ (𝐵‘𝑚) ∈ dom card) → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 139 | 96, 96, 138 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘𝑚) ∈ Fin → ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚)))) |
| 140 | 139 | ensymd 9045 |
. . . . . . . . . . . 12
⊢ ((𝐵‘𝑚) ∈ Fin → ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ≈ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) |
| 141 | 140 | adantl 481 |
. . . . . . . . . . 11
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ≈ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) |
| 142 | | sdomentr 9151 |
. . . . . . . . . . 11
⊢
(((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≺ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ∧ ((card‘(𝐵‘𝑚)) +o (card‘(𝐵‘𝑚))) ≈ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) |
| 143 | 137, 141,
142 | syl2anc 584 |
. . . . . . . . . 10
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) |
| 144 | | domsdomtr 9152 |
. . . . . . . . . 10
⊢
((∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≼ (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ∧ (∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ⊔ (𝐵‘𝑚)) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) → ∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) |
| 145 | 89, 143, 144 | sylancr 587 |
. . . . . . . . 9
⊢
((∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) ∧ (𝐵‘𝑚) ∈ Fin) → ∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚))) |
| 146 | 145 | expcom 413 |
. . . . . . . 8
⊢ ((𝐵‘𝑚) ∈ Fin → (∪ 𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)))) |
| 147 | 82, 146 | syl 17 |
. . . . . . 7
⊢ ((𝑚 ∈ ω ∧
∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) → (∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)))) |
| 148 | | sdomentr 9151 |
. . . . . . . 8
⊢
((∪ 𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ∧ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝐵‘suc 𝑚)) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚)) |
| 149 | 148 | expcom 413 |
. . . . . . 7
⊢ (((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) ≈ (𝐵‘suc 𝑚) → (∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ ((𝐵‘𝑚) ⊔ (𝐵‘𝑚)) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚))) |
| 150 | 72, 147, 149 | sylsyld 61 |
. . . . . 6
⊢ ((𝑚 ∈ ω ∧
∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) → (∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚))) |
| 151 | 38, 150 | syld 47 |
. . . . 5
⊢ ((𝑚 ∈ ω ∧
∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘) → ((∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚))) |
| 152 | 151 | ex 412 |
. . . 4
⊢ (𝑚 ∈ ω →
(∀𝑘 ∈ suc suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ((∀𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚)))) |
| 153 | 152 | com23 86 |
. . 3
⊢ (𝑚 ∈ ω →
((∀𝑘 ∈ suc
𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑚 (𝐵‘𝑘) ≺ (𝐵‘𝑚)) → (∀𝑘 ∈ suc suc 𝑚(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ suc 𝑚(𝐵‘𝑘) ≺ (𝐵‘suc 𝑚)))) |
| 154 | 6, 12, 18, 32, 153 | finds1 7921 |
. 2
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛))) |
| 155 | 154 | imp 406 |
1
⊢ ((𝑛 ∈ ω ∧
∀𝑘 ∈ suc 𝑛(𝐵‘𝑘) ≈ 𝒫 𝑘) → ∪
𝑘 ∈ 𝑛 (𝐵‘𝑘) ≺ (𝐵‘𝑛)) |