Step | Hyp | Ref
| Expression |
1 | | elex 3212 |
. 2
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V) |
2 | | limsuc 7049 |
. . . . . . . . . . . . . . . . . 18
⊢ (Lim
𝐴 → (𝑣 ∈ 𝐴 ↔ suc 𝑣 ∈ 𝐴)) |
3 | 2 | biimpd 219 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝐴 → (𝑣 ∈ 𝐴 → suc 𝑣 ∈ 𝐴)) |
4 | | sseq1 3626 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = suc 𝑣 → (𝑧 ⊆ 𝑤 ↔ suc 𝑣 ⊆ 𝑤)) |
5 | 4 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = suc 𝑣 → (∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃𝑤 ∈ 𝑦 suc 𝑣 ⊆ 𝑤)) |
6 | 5 | rspcv 3305 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑣 ∈ 𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ∃𝑤 ∈ 𝑦 suc 𝑣 ⊆ 𝑤)) |
7 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑣 ∈ V |
8 | | sucssel 5819 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ V → (suc 𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑤)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (suc
𝑣 ⊆ 𝑤 → 𝑣 ∈ 𝑤) |
10 | 9 | reximi 3011 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑤 ∈
𝑦 suc 𝑣 ⊆ 𝑤 → ∃𝑤 ∈ 𝑦 𝑣 ∈ 𝑤) |
11 | | eluni2 4440 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ ∪ 𝑦
↔ ∃𝑤 ∈
𝑦 𝑣 ∈ 𝑤) |
12 | 10, 11 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑤 ∈
𝑦 suc 𝑣 ⊆ 𝑤 → 𝑣 ∈ ∪ 𝑦) |
13 | 6, 12 | syl6com 37 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → (suc 𝑣 ∈ 𝐴 → 𝑣 ∈ ∪ 𝑦)) |
14 | 3, 13 | syl9 77 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → (𝑣 ∈ 𝐴 → 𝑣 ∈ ∪ 𝑦))) |
15 | 14 | ralrimdv 2968 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → ∀𝑣 ∈ 𝐴 𝑣 ∈ ∪ 𝑦)) |
16 | | dfss3 3592 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ ∪ 𝑦
↔ ∀𝑣 ∈
𝐴 𝑣 ∈ ∪ 𝑦) |
17 | 15, 16 | syl6ibr 242 |
. . . . . . . . . . . . . 14
⊢ (Lim
𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → 𝐴 ⊆ ∪ 𝑦)) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴) → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → 𝐴 ⊆ ∪ 𝑦)) |
19 | | uniss 4458 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ 𝐴 → ∪ 𝑦 ⊆ ∪ 𝐴) |
20 | | limuni 5785 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝐴 → 𝐴 = ∪ 𝐴) |
21 | 20 | sseq2d 3633 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝐴 → (∪ 𝑦
⊆ 𝐴 ↔ ∪ 𝑦
⊆ ∪ 𝐴)) |
22 | 19, 21 | syl5ibr 236 |
. . . . . . . . . . . . . 14
⊢ (Lim
𝐴 → (𝑦 ⊆ 𝐴 → ∪ 𝑦 ⊆ 𝐴)) |
23 | 22 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴) → ∪ 𝑦 ⊆ 𝐴) |
24 | 18, 23 | jctird 567 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴) → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → (𝐴 ⊆ ∪ 𝑦 ∧ ∪ 𝑦
⊆ 𝐴))) |
25 | | eqss 3618 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∪
𝑦 ↔ (𝐴 ⊆ ∪ 𝑦 ∧ ∪ 𝑦
⊆ 𝐴)) |
26 | 24, 25 | syl6ibr 242 |
. . . . . . . . . . 11
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴) → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 → 𝐴 = ∪ 𝑦)) |
27 | 26 | imdistanda 729 |
. . . . . . . . . 10
⊢ (Lim
𝐴 → ((𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤) → (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))) |
28 | 27 | anim2d 589 |
. . . . . . . . 9
⊢ (Lim
𝐴 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → (𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)))) |
29 | 28 | eximdv 1846 |
. . . . . . . 8
⊢ (Lim
𝐴 → (∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)))) |
30 | 29 | ss2abdv 3675 |
. . . . . . 7
⊢ (Lim
𝐴 → {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
31 | | intss 4498 |
. . . . . . 7
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))} ⊆ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
33 | 32 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
34 | | limelon 5788 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → 𝐴 ∈ On) |
35 | | cfval 9069 |
. . . . . 6
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (cf‘𝐴) = ∩
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤))}) |
37 | 33, 36 | sseqtr4d 3642 |
. . . 4
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ (cf‘𝐴)) |
38 | | cfub 9071 |
. . . . 5
⊢
(cf‘𝐴) ⊆
∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} |
39 | | eqimss 3657 |
. . . . . . . . . 10
⊢ (𝐴 = ∪
𝑦 → 𝐴 ⊆ ∪ 𝑦) |
40 | 39 | anim2i 593 |
. . . . . . . . 9
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦) → (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦)) |
41 | 40 | anim2i 593 |
. . . . . . . 8
⊢ ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → (𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))) |
42 | 41 | eximi 1762 |
. . . . . . 7
⊢
(∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))) |
43 | 42 | ss2abi 3674 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} |
44 | | intss 4498 |
. . . . . 6
⊢ ({𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} → ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
45 | 43, 44 | ax-mp 5 |
. . . . 5
⊢ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦))} ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} |
46 | 38, 45 | sstri 3612 |
. . . 4
⊢
(cf‘𝐴) ⊆
∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} |
47 | 37, 46 | jctil 560 |
. . 3
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → ((cf‘𝐴) ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∧ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ (cf‘𝐴))) |
48 | | eqss 3618 |
. . 3
⊢
((cf‘𝐴) =
∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ↔ ((cf‘𝐴) ⊆ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ∧ ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))} ⊆ (cf‘𝐴))) |
49 | 47, 48 | sylibr 224 |
. 2
⊢ ((𝐴 ∈ V ∧ Lim 𝐴) → (cf‘𝐴) = ∩
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |
50 | 1, 49 | sylan 488 |
1
⊢ ((𝐴 ∈ 𝐵 ∧ Lim 𝐴) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ 𝐴 = ∪ 𝑦))}) |