| Step | Hyp | Ref
| Expression |
| 1 | | cfss.1 |
. . . . . 6
⊢ 𝐴 ∈ V |
| 2 | 1 | cflim3 10302 |
. . . . 5
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥)) |
| 3 | | fvex 6919 |
. . . . . . 7
⊢
(card‘𝑥)
∈ V |
| 4 | 3 | dfiin2 5034 |
. . . . . 6
⊢ ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) = ∩ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} |
| 5 | | cardon 9984 |
. . . . . . . . . 10
⊢
(card‘𝑥)
∈ On |
| 6 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑦 = (card‘𝑥) → (𝑦 ∈ On ↔ (card‘𝑥) ∈ On)) |
| 7 | 5, 6 | mpbiri 258 |
. . . . . . . . 9
⊢ (𝑦 = (card‘𝑥) → 𝑦 ∈ On) |
| 8 | 7 | rexlimivw 3151 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥) → 𝑦 ∈ On) |
| 9 | 8 | abssi 4070 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ⊆ On |
| 10 | | limuni 6445 |
. . . . . . . . . . . 12
⊢ (Lim
𝐴 → 𝐴 = ∪ 𝐴) |
| 11 | 10 | eqcomd 2743 |
. . . . . . . . . . 11
⊢ (Lim
𝐴 → ∪ 𝐴 =
𝐴) |
| 12 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → (card‘𝑥) = (card‘𝐴)) |
| 13 | 12 | eqcomd 2743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (card‘𝐴) = (card‘𝑥)) |
| 14 | 13 | biantrud 531 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → (∪ 𝐴 = 𝐴 ↔ (∪ 𝐴 = 𝐴 ∧ (card‘𝐴) = (card‘𝑥)))) |
| 15 | | unieq 4918 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪
𝐴) |
| 16 | 15 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → (∪ 𝑥 = 𝐴 ↔ ∪ 𝐴 = 𝐴)) |
| 17 | 1 | pwid 4622 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐴 ∈ 𝒫 𝐴 |
| 18 | | eleq1 2829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝒫 𝐴 ↔ 𝐴 ∈ 𝒫 𝐴)) |
| 19 | 17, 18 | mpbiri 258 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐴 → 𝑥 ∈ 𝒫 𝐴) |
| 20 | 19 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐴 → (∪ 𝑥 = 𝐴 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴))) |
| 21 | 16, 20 | bitr3d 281 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐴 → (∪ 𝐴 = 𝐴 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴))) |
| 22 | 21 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐴 → ((∪ 𝐴 = 𝐴 ∧ (card‘𝐴) = (card‘𝑥)) ↔ ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)))) |
| 23 | 14, 22 | bitr2d 280 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐴 → (((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥)) ↔ ∪ 𝐴 = 𝐴)) |
| 24 | 1, 23 | spcev 3606 |
. . . . . . . . . . 11
⊢ (∪ 𝐴 =
𝐴 → ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥))) |
| 25 | 11, 24 | syl 17 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥))) |
| 26 | | df-rex 3071 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝐴) = (card‘𝑥) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝐴) = (card‘𝑥))) |
| 27 | | rabid 3458 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ↔ (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
| 28 | 27 | anbi1i 624 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝐴) = (card‘𝑥)) ↔ ((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥))) |
| 29 | 28 | exbii 1848 |
. . . . . . . . . . 11
⊢
(∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (card‘𝐴) = (card‘𝑥)) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥))) |
| 30 | 26, 29 | bitri 275 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝐴) = (card‘𝑥) ↔ ∃𝑥((𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴) ∧ (card‘𝐴) = (card‘𝑥))) |
| 31 | 25, 30 | sylibr 234 |
. . . . . . . . 9
⊢ (Lim
𝐴 → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥)) |
| 32 | | fvex 6919 |
. . . . . . . . . 10
⊢
(card‘𝐴)
∈ V |
| 33 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑦 = (card‘𝐴) → (𝑦 = (card‘𝑥) ↔ (card‘𝐴) = (card‘𝑥))) |
| 34 | 33 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑦 = (card‘𝐴) → (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝐴) = (card‘𝑥))) |
| 35 | 32, 34 | spcev 3606 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (card‘𝐴) = (card‘𝑥) → ∃𝑦∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)) |
| 36 | 31, 35 | syl 17 |
. . . . . . . 8
⊢ (Lim
𝐴 → ∃𝑦∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)) |
| 37 | | abn0 4385 |
. . . . . . . 8
⊢ ({𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ≠ ∅ ↔ ∃𝑦∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)) |
| 38 | 36, 37 | sylibr 234 |
. . . . . . 7
⊢ (Lim
𝐴 → {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ≠ ∅) |
| 39 | | onint 7810 |
. . . . . . 7
⊢ (({𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ⊆ On ∧ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ≠ ∅) → ∩ {𝑦
∣ ∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)}) |
| 40 | 9, 38, 39 | sylancr 587 |
. . . . . 6
⊢ (Lim
𝐴 → ∩ {𝑦
∣ ∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴}𝑦 = (card‘𝑥)} ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)}) |
| 41 | 4, 40 | eqeltrid 2845 |
. . . . 5
⊢ (Lim
𝐴 → ∩ 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (card‘𝑥) ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)}) |
| 42 | 2, 41 | eqeltrd 2841 |
. . . 4
⊢ (Lim
𝐴 → (cf‘𝐴) ∈ {𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)}) |
| 43 | | fvex 6919 |
. . . . 5
⊢
(cf‘𝐴) ∈
V |
| 44 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑦 = (cf‘𝐴) → (𝑦 = (card‘𝑥) ↔ (cf‘𝐴) = (card‘𝑥))) |
| 45 | 44 | rexbidv 3179 |
. . . . 5
⊢ (𝑦 = (cf‘𝐴) → (∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥) ↔ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥))) |
| 46 | 43, 45 | elab 3679 |
. . . 4
⊢
((cf‘𝐴) ∈
{𝑦 ∣ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}𝑦 = (card‘𝑥)} ↔ ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥)) |
| 47 | 42, 46 | sylib 218 |
. . 3
⊢ (Lim
𝐴 → ∃𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} (cf‘𝐴) = (card‘𝑥)) |
| 48 | | df-rex 3071 |
. . 3
⊢
(∃𝑥 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 =
𝐴} (cf‘𝐴) = (card‘𝑥) ↔ ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) |
| 49 | 47, 48 | sylib 218 |
. 2
⊢ (Lim
𝐴 → ∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) |
| 50 | | simprl 771 |
. . . . . . . 8
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴}) |
| 51 | 50, 27 | sylib 218 |
. . . . . . 7
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → (𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴)) |
| 52 | 51 | simpld 494 |
. . . . . 6
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ∈ 𝒫 𝐴) |
| 53 | 52 | elpwid 4609 |
. . . . 5
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ⊆ 𝐴) |
| 54 | | simpl 482 |
. . . . . . 7
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → Lim 𝐴) |
| 55 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 56 | | limord 6444 |
. . . . . . . . . . . 12
⊢ (Lim
𝐴 → Ord 𝐴) |
| 57 | | ordsson 7803 |
. . . . . . . . . . . 12
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (Lim
𝐴 → 𝐴 ⊆ On) |
| 59 | | sstr 3992 |
. . . . . . . . . . 11
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑥 ⊆ On) |
| 60 | 58, 59 | sylan2 593 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ 𝐴 ∧ Lim 𝐴) → 𝑥 ⊆ On) |
| 61 | | onssnum 10080 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ V ∧ 𝑥 ⊆ On) → 𝑥 ∈ dom
card) |
| 62 | 55, 60, 61 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ 𝐴 ∧ Lim 𝐴) → 𝑥 ∈ dom card) |
| 63 | | cardid2 9993 |
. . . . . . . . 9
⊢ (𝑥 ∈ dom card →
(card‘𝑥) ≈
𝑥) |
| 64 | 62, 63 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ Lim 𝐴) → (card‘𝑥) ≈ 𝑥) |
| 65 | 64 | ensymd 9045 |
. . . . . . 7
⊢ ((𝑥 ⊆ 𝐴 ∧ Lim 𝐴) → 𝑥 ≈ (card‘𝑥)) |
| 66 | 53, 54, 65 | syl2anc 584 |
. . . . . 6
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ≈ (card‘𝑥)) |
| 67 | | simprr 773 |
. . . . . 6
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → (cf‘𝐴) = (card‘𝑥)) |
| 68 | 66, 67 | breqtrrd 5171 |
. . . . 5
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → 𝑥 ≈ (cf‘𝐴)) |
| 69 | 51 | simprd 495 |
. . . . 5
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → ∪ 𝑥 = 𝐴) |
| 70 | 53, 68, 69 | 3jca 1129 |
. . . 4
⊢ ((Lim
𝐴 ∧ (𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥))) → (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴)) |
| 71 | 70 | ex 412 |
. . 3
⊢ (Lim
𝐴 → ((𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥)) → (𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴))) |
| 72 | 71 | eximdv 1917 |
. 2
⊢ (Lim
𝐴 → (∃𝑥(𝑥 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴} ∧ (cf‘𝐴) = (card‘𝑥)) → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴))) |
| 73 | 49, 72 | mpd 15 |
1
⊢ (Lim
𝐴 → ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ (cf‘𝐴) ∧ ∪ 𝑥 = 𝐴)) |