Step | Hyp | Ref
| Expression |
1 | | cfval 9658 |
. . . 4
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
2 | | vex 3444 |
. . . . . . . . 9
⊢ 𝑣 ∈ V |
3 | | eqeq1 2802 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (𝑥 = (card‘𝑦) ↔ 𝑣 = (card‘𝑦))) |
4 | 3 | anbi1d 632 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ (𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
5 | 4 | exbidv 1922 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)))) |
6 | 2, 5 | elab 3615 |
. . . . . . . 8
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ↔ ∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))) |
7 | | fveq2 6645 |
. . . . . . . . . . . 12
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) =
(card‘(card‘𝑦))) |
8 | | cardidm 9372 |
. . . . . . . . . . . 12
⊢
(card‘(card‘𝑦)) = (card‘𝑦) |
9 | 7, 8 | eqtrdi 2849 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = (card‘𝑦)) |
10 | | eqeq2 2810 |
. . . . . . . . . . 11
⊢ (𝑣 = (card‘𝑦) → ((card‘𝑣) = 𝑣 ↔ (card‘𝑣) = (card‘𝑦))) |
11 | 9, 10 | mpbird 260 |
. . . . . . . . . 10
⊢ (𝑣 = (card‘𝑦) → (card‘𝑣) = 𝑣) |
12 | 11 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
13 | 12 | exlimiv 1931 |
. . . . . . . 8
⊢
(∃𝑦(𝑣 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (card‘𝑣) = 𝑣) |
14 | 6, 13 | sylbi 220 |
. . . . . . 7
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → (card‘𝑣) = 𝑣) |
15 | | cardon 9357 |
. . . . . . 7
⊢
(card‘𝑣)
∈ On |
16 | 14, 15 | eqeltrrdi 2899 |
. . . . . 6
⊢ (𝑣 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → 𝑣 ∈ On) |
17 | 16 | ssriv 3919 |
. . . . 5
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On |
18 | | fvex 6658 |
. . . . . . 7
⊢
(cf‘𝐴) ∈
V |
19 | 1, 18 | eqeltrrdi 2899 |
. . . . . 6
⊢ (𝐴 ∈ On → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ V) |
20 | | intex 5204 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ≠ ∅ ↔ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ V) |
21 | 19, 20 | sylibr 237 |
. . . . 5
⊢ (𝐴 ∈ On → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ≠ ∅) |
22 | | onint 7490 |
. . . . 5
⊢ (({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ On ∧ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ≠ ∅) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
23 | 17, 21, 22 | sylancr 590 |
. . . 4
⊢ (𝐴 ∈ On → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
24 | 1, 23 | eqeltrd 2890 |
. . 3
⊢ (𝐴 ∈ On →
(cf‘𝐴) ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
25 | | fveq2 6645 |
. . . . 5
⊢ (𝑣 = (cf‘𝐴) → (card‘𝑣) = (card‘(cf‘𝐴))) |
26 | | id 22 |
. . . . 5
⊢ (𝑣 = (cf‘𝐴) → 𝑣 = (cf‘𝐴)) |
27 | 25, 26 | eqeq12d 2814 |
. . . 4
⊢ (𝑣 = (cf‘𝐴) → ((card‘𝑣) = 𝑣 ↔ (card‘(cf‘𝐴)) = (cf‘𝐴))) |
28 | 27, 14 | vtoclga 3522 |
. . 3
⊢
((cf‘𝐴) ∈
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} → (card‘(cf‘𝐴)) = (cf‘𝐴)) |
29 | 24, 28 | syl 17 |
. 2
⊢ (𝐴 ∈ On →
(card‘(cf‘𝐴)) =
(cf‘𝐴)) |
30 | | cff 9659 |
. . . . . 6
⊢
cf:On⟶On |
31 | 30 | fdmi 6498 |
. . . . 5
⊢ dom cf =
On |
32 | 31 | eleq2i 2881 |
. . . 4
⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On) |
33 | | ndmfv 6675 |
. . . 4
⊢ (¬
𝐴 ∈ dom cf →
(cf‘𝐴) =
∅) |
34 | 32, 33 | sylnbir 334 |
. . 3
⊢ (¬
𝐴 ∈ On →
(cf‘𝐴) =
∅) |
35 | | card0 9371 |
. . . 4
⊢
(card‘∅) = ∅ |
36 | | fveq2 6645 |
. . . 4
⊢
((cf‘𝐴) =
∅ → (card‘(cf‘𝐴)) = (card‘∅)) |
37 | | id 22 |
. . . 4
⊢
((cf‘𝐴) =
∅ → (cf‘𝐴)
= ∅) |
38 | 35, 36, 37 | 3eqtr4a 2859 |
. . 3
⊢
((cf‘𝐴) =
∅ → (card‘(cf‘𝐴)) = (cf‘𝐴)) |
39 | 34, 38 | syl 17 |
. 2
⊢ (¬
𝐴 ∈ On →
(card‘(cf‘𝐴)) =
(cf‘𝐴)) |
40 | 29, 39 | pm2.61i 185 |
1
⊢
(card‘(cf‘𝐴)) = (cf‘𝐴) |