Step | Hyp | Ref
| Expression |
1 | | limord 6088 |
. . . 4
⊢ (Lim
𝐴 → Ord 𝐴) |
2 | | cflim3.1 |
. . . . 5
⊢ 𝐴 ∈ V |
3 | 2 | elon 6038 |
. . . 4
⊢ (𝐴 ∈ On ↔ Ord 𝐴) |
4 | 1, 3 | sylibr 226 |
. . 3
⊢ (Lim
𝐴 → 𝐴 ∈ On) |
5 | | cfval 9467 |
. . 3
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑦
∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
6 | 4, 5 | syl 17 |
. 2
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩
{𝑦 ∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
7 | | fvex 6512 |
. . . 4
⊢
(card‘𝑥)
∈ V |
8 | 7 | dfiin2 4829 |
. . 3
⊢ ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} |
9 | | df-rex 3094 |
. . . . . 6
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥))) |
10 | | ancom 453 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥)) ↔ (𝑦 = (card‘𝑥) ∧ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴})) |
11 | | rabid 3317 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
12 | | selpw 4429 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
13 | 12 | anbi1i 614 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 =
𝐴) ↔ (𝑥 ⊆ 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
14 | | coflim 9481 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑥 ⊆ 𝐴) → (∪ 𝑥 = 𝐴 ↔ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)) |
15 | 14 | pm5.32da 571 |
. . . . . . . . . . 11
⊢ (Lim
𝐴 → ((𝑥 ⊆ 𝐴 ∧ ∪ 𝑥 = 𝐴) ↔ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))) |
16 | 13, 15 | syl5bb 275 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 =
𝐴) ↔ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))) |
17 | 11, 16 | syl5bb 275 |
. . . . . . . . 9
⊢ (Lim
𝐴 → (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))) |
18 | 17 | anbi2d 619 |
. . . . . . . 8
⊢ (Lim
𝐴 → ((𝑦 = (card‘𝑥) ∧ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}) ↔ (𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
19 | 10, 18 | syl5bb 275 |
. . . . . . 7
⊢ (Lim
𝐴 → ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥)) ↔ (𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
20 | 19 | exbidv 1880 |
. . . . . 6
⊢ (Lim
𝐴 → (∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ 𝑦 = (card‘𝑥)) ↔ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
21 | 9, 20 | syl5bb 275 |
. . . . 5
⊢ (Lim
𝐴 → (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤)))) |
22 | 21 | abbidv 2843 |
. . . 4
⊢ (Lim
𝐴 → {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} = {𝑦 ∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
23 | 22 | inteqd 4754 |
. . 3
⊢ (Lim
𝐴 → ∩ {𝑦
∣ ∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥)} = ∩ {𝑦 ∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))}) |
24 | 8, 23 | syl5req 2827 |
. 2
⊢ (Lim
𝐴 → ∩ {𝑦
∣ ∃𝑥(𝑦 = (card‘𝑥) ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑥 𝑧 ⊆ 𝑤))} = ∩
𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝑥)) |
25 | 6, 24 | eqtrd 2814 |
1
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) |