| Step | Hyp | Ref
| Expression |
| 1 | | limord 6444 |
. . . 4
⊢ (Lim
𝐴 → Ord 𝐴) |
| 2 | | cflim3.1 |
. . . . 5
⊢ 𝐴 ∈ V |
| 3 | 2 | elon 6393 |
. . . 4
⊢ (𝐴 ∈ On ↔ Ord 𝐴) |
| 4 | 1, 3 | sylibr 234 |
. . 3
⊢ (Lim
𝐴 → 𝐴 ∈ On) |
| 5 | | cfval 10287 |
. . 3
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑦
∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
| 6 | 4, 5 | syl 17 |
. 2
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩
{𝑦 ∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
| 7 | | fvex 6919 |
. . . 4
⊢
(card‘𝑥)
∈ V |
| 8 | 7 | dfiin2 5034 |
. . 3
⊢ ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} |
| 9 | | df-rex 3071 |
. . . . . 6
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥))) |
| 10 | | ancom 460 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥)) ↔ (𝑦 = (card‘𝑥) ∧ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴})) |
| 11 | | rabid 3458 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
| 12 | | velpw 4605 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 13 | 12 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 =
𝐴) ↔ (𝑥 ⊆ 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
| 14 | | coflim 10301 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝑥 = 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)) |
| 15 | 14 | pm5.32da 579 |
. . . . . . . . . . 11
⊢ (Lim
𝐴 → ((𝑥 ⊆ 𝐴 ∧ ∪ 𝑥 = 𝐴) ↔ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))) |
| 16 | 13, 15 | bitrid 283 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 =
𝐴) ↔ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))) |
| 17 | 11, 16 | bitrid 283 |
. . . . . . . . 9
⊢ (Lim
𝐴 → (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))) |
| 18 | 17 | anbi2d 630 |
. . . . . . . 8
⊢ (Lim
𝐴 → ((𝑦 = (card‘𝑥) ∧ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}) ↔ (𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
| 19 | 10, 18 | bitrid 283 |
. . . . . . 7
⊢ (Lim
𝐴 → ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥)) ↔ (𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
| 20 | 19 | exbidv 1921 |
. . . . . 6
⊢ (Lim
𝐴 → (∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥)) ↔ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
| 21 | 9, 20 | bitrid 283 |
. . . . 5
⊢ (Lim
𝐴 → (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
| 22 | 21 | abbidv 2808 |
. . . 4
⊢ (Lim
𝐴 → {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} = {𝑦 ∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
| 23 | 22 | inteqd 4951 |
. . 3
⊢ (Lim
𝐴 → ∩ {𝑦
∣ ∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥)} = ∩ {𝑦 ∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
| 24 | 8, 23 | eqtr2id 2790 |
. 2
⊢ (Lim
𝐴 → ∩ {𝑦
∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))} = ∩
𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥)) |
| 25 | 6, 24 | eqtrd 2777 |
1
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) |