| Step | Hyp | Ref
| Expression |
| 1 | | cfval 10287 |
. . . 4
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
| 2 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
| 3 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝑥 = (card‘𝑦) ↔ 𝑣 = (card‘𝑦))) |
| 4 | 3 | anbi1d 631 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
| 5 | 4 | exbidv 1921 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
| 6 | 2, 5 | elab 3679 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
| 7 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) =
(card‘(card‘𝑦))) |
| 8 | | cardidm 9999 |
. . . . . . . . . . . 12
⊢
(card‘(card‘𝑦)) = (card‘𝑦) |
| 9 | 7, 8 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = (card‘𝑦)) |
| 10 | | eqeq2 2749 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → ((card‘𝑣) = 𝑣 ↔ (card‘𝑣) = (card‘𝑦))) |
| 11 | 9, 10 | mpbird 257 |
. . . . . . . . . 10
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = 𝑣) |
| 12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
| 13 | 12 | exlimiv 1930 |
. . . . . . . 8
⊢
(∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
| 14 | 6, 13 | sylbi 217 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → (card‘𝑣) = 𝑣) |
| 15 | | cardon 9984 |
. . . . . . 7
⊢
(card‘𝑣)
∈ On |
| 16 | 14, 15 | eqeltrrdi 2850 |
. . . . . 6
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → 𝑣 ∈ On) |
| 17 | 16 | ssriv 3987 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On |
| 18 | | fvex 6919 |
. . . . . . 7
⊢
(cf‘𝐴) ∈
V |
| 19 | 1, 18 | eqeltrrdi 2850 |
. . . . . 6
⊢ (𝐴 ∈ On → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ V) |
| 20 | | intex 5344 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ≠ ∅ ↔ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ V) |
| 21 | 19, 20 | sylibr 234 |
. . . . 5
⊢ (𝐴 ∈ On → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ≠ ∅) |
| 22 | | onint 7810 |
. . . . 5
⊢ (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
| 23 | 17, 21, 22 | sylancr 587 |
. . . 4
⊢ (𝐴 ∈ On → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
| 24 | 1, 23 | eqeltrd 2841 |
. . 3
⊢ (𝐴 ∈ On →
(cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
| 25 | | fveq2 6906 |
. . . . 5
⊢ (𝑣 = (cf‘𝐴) → (card‘𝑣) = (card‘(cf‘𝐴))) |
| 26 | | id 22 |
. . . . 5
⊢ (𝑣 = (cf‘𝐴) → 𝑣 = (cf‘𝐴)) |
| 27 | 25, 26 | eqeq12d 2753 |
. . . 4
⊢ (𝑣 = (cf‘𝐴) → ((card‘𝑣) = 𝑣 ↔ (card‘(cf‘𝐴)) = (cf‘𝐴))) |
| 28 | 27, 14 | vtoclga 3577 |
. . 3
⊢
((cf‘𝐴) ∈
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → (card‘(cf‘𝐴)) = (cf‘𝐴)) |
| 29 | 24, 28 | syl 17 |
. 2
⊢ (𝐴 ∈ On →
(card‘(cf‘𝐴)) =
(cf‘𝐴)) |
| 30 | | cff 10288 |
. . . . . 6
⊢
cf:On⟶On |
| 31 | 30 | fdmi 6747 |
. . . . 5
⊢ dom cf =
On |
| 32 | 31 | eleq2i 2833 |
. . . 4
⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On) |
| 33 | | ndmfv 6941 |
. . . 4
⊢ (¬
𝐴 ∈ dom cf →
(cf‘𝐴) =
∅) |
| 34 | 32, 33 | sylnbir 331 |
. . 3
⊢ (¬
𝐴 ∈ On →
(cf‘𝐴) =
∅) |
| 35 | | card0 9998 |
. . . 4
⊢
(card‘∅) = ∅ |
| 36 | | fveq2 6906 |
. . . 4
⊢
((cf‘𝐴) =
∅ → (card‘(cf‘𝐴)) = (card‘∅)) |
| 37 | | id 22 |
. . . 4
⊢
((cf‘𝐴) =
∅ → (cf‘𝐴)
= ∅) |
| 38 | 35, 36, 37 | 3eqtr4a 2803 |
. . 3
⊢
((cf‘𝐴) =
∅ → (card‘(cf‘𝐴)) = (cf‘𝐴)) |
| 39 | 34, 38 | syl 17 |
. 2
⊢ (¬
𝐴 ∈ On →
(card‘(cf‘𝐴)) =
(cf‘𝐴)) |
| 40 | 29, 39 | pm2.61i 182 |
1
⊢
(card‘(cf‘𝐴)) = (cf‘𝐴) |