Step | Hyp | Ref
| Expression |
1 | | rabid 3326 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) |
2 | | selpw 4385 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
3 | | limord 6022 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
𝐴 → Ord 𝐴) |
4 | | ordsson 7250 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
5 | | sstr 3835 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On) |
6 | 5 | expcom 404 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆ On → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On)) |
7 | 3, 4, 6 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
𝐴 → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On)) |
8 | 7 | imp 397 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
9 | 8 | 3adant3 1166 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ⊆ On) |
10 | | ssel2 3822 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On) |
11 | | eloni 5973 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ On → Ord 𝑠) |
12 | | ordirr 5981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑠 → ¬ 𝑠 ∈ 𝑠) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠) |
14 | | ssel 3821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ⊆ 𝑠 → (𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠)) |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ 𝑦 → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠)) |
16 | 15 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠)) |
17 | 13, 16 | mtod 190 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠) |
18 | 9, 17 | sylan 575 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠) |
19 | | simpl2 1248 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → 𝑦 ⊆ 𝐴) |
20 | | sstr 3835 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠) |
21 | 19, 20 | sylan 575 |
. . . . . . . . . . . . . . . 16
⊢ ((((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠) |
22 | 18, 21 | mtand 850 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠) |
23 | | simpl3 1250 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴) |
24 | 23 | sseq1d 3857 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠)) |
25 | 22, 24 | mtbird 317 |
. . . . . . . . . . . . . 14
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪
𝑦 ⊆ 𝑠) |
26 | | unissb 4691 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦
⊆ 𝑠 ↔
∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠) |
27 | 25, 26 | sylnib 320 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠) |
28 | 27 | nrexdv 3209 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠) |
29 | | ssel 3821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On)) |
30 | | ssel 3821 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On)) |
31 | | ontri1 5997 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)) |
32 | 31 | ancoms 452 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)) |
33 | | vex 3417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑡 ∈ V |
34 | | vex 3417 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑠 ∈ V |
35 | 33, 34 | brcnv 5537 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡) |
36 | | epel 5258 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡) |
37 | 35, 36 | bitri 267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡◡ E 𝑠 ↔ 𝑠 ∈ 𝑡) |
38 | 37 | notbii 312 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑡◡ E 𝑠 ↔ ¬ 𝑠 ∈ 𝑡) |
39 | 32, 38 | syl6bbr 281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠)) |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠))) |
41 | 29, 30, 40 | syl2and 601 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ On → ((𝑠 ∈ 𝑦 ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠))) |
42 | 41 | impl 449 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠)) |
43 | 42 | ralbidva 3194 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠)) |
44 | 43 | rexbidva 3259 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠)) |
45 | 9, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠)) |
46 | 28, 45 | mtbid 316 |
. . . . . . . . . . 11
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠) |
47 | | vex 3417 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V) |
49 | | epweon 7243 |
. . . . . . . . . . . . . . . . . . 19
⊢ E We
On |
50 | | wess 5329 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ⊆ On → ( E We On
→ E We 𝑦)) |
51 | 49, 50 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ⊆ On → E We 𝑦) |
52 | | weso 5333 |
. . . . . . . . . . . . . . . . . 18
⊢ ( E We
𝑦 → E Or 𝑦) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → E Or 𝑦) |
54 | | cnvso 5915 |
. . . . . . . . . . . . . . . . 17
⊢ ( E Or
𝑦 ↔ ◡ E Or 𝑦) |
55 | 53, 54 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ On → ◡ E Or 𝑦) |
56 | 55 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → ◡ E Or 𝑦) |
57 | | onssnum 9176 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom
card) |
58 | 47, 57 | mpan 681 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ⊆ On → 𝑦 ∈ dom
card) |
59 | | cardid2 9092 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ dom card →
(card‘𝑦) ≈
𝑦) |
60 | | ensym 8271 |
. . . . . . . . . . . . . . . . . 18
⊢
((card‘𝑦)
≈ 𝑦 → 𝑦 ≈ (card‘𝑦)) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦)) |
62 | | nnsdom 8828 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘𝑦)
∈ ω → (card‘𝑦) ≺ ω) |
63 | | ensdomtr 8365 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺
ω) |
64 | 61, 62, 63 | syl2an 589 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → 𝑦 ≺
ω) |
65 | | isfinite 8826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺
ω) |
66 | 64, 65 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → 𝑦 ∈
Fin) |
67 | | wofi 8478 |
. . . . . . . . . . . . . . 15
⊢ ((◡ E Or 𝑦 ∧ 𝑦 ∈ Fin) → ◡ E We 𝑦) |
68 | 56, 66, 67 | syl2anc 579 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → ◡ E We 𝑦) |
69 | 9, 68 | sylan 575 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦) |
70 | | wefr 5332 |
. . . . . . . . . . . . 13
⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦) |
72 | | ssidd 3849 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦) |
73 | | unieq 4666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∪ ∅) |
74 | | uni0 4687 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ ∅ = ∅ |
75 | 73, 74 | syl6eq 2877 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∅) |
76 | | eqeq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 =
𝐴 → (∪ 𝑦 =
∅ ↔ 𝐴 =
∅)) |
77 | 75, 76 | syl5ib 236 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑦 =
𝐴 → (𝑦 = ∅ → 𝐴 = ∅)) |
78 | | nlim0 6021 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
Lim ∅ |
79 | | limeq 5975 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim
∅)) |
80 | 78, 79 | mtbiri 319 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = ∅ → ¬ Lim
𝐴) |
81 | 77, 80 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑦 =
𝐴 → (𝑦 = ∅ → ¬ Lim
𝐴)) |
82 | 81 | necon2ad 3014 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑦 =
𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅)) |
83 | 82 | impcom 398 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝐴 ∧ ∪ 𝑦 =
𝐴) → 𝑦 ≠ ∅) |
84 | 83 | 3adant2 1165 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅) |
85 | 84 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅) |
86 | | fri 5304 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ V ∧ ◡ E Fr 𝑦) ∧ (𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅)) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠) |
87 | 48, 71, 72, 85, 86 | syl22anc 872 |
. . . . . . . . . . 11
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠) |
88 | 46, 87 | mtand 850 |
. . . . . . . . . 10
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈
ω) |
89 | | cardon 9083 |
. . . . . . . . . . 11
⊢
(card‘𝑦)
∈ On |
90 | | eloni 5973 |
. . . . . . . . . . 11
⊢
((card‘𝑦)
∈ On → Ord (card‘𝑦)) |
91 | | ordom 7335 |
. . . . . . . . . . . 12
⊢ Ord
ω |
92 | | ordtri1 5996 |
. . . . . . . . . . . 12
⊢ ((Ord
ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈
ω)) |
93 | 91, 92 | mpan 681 |
. . . . . . . . . . 11
⊢ (Ord
(card‘𝑦) →
(ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)) |
94 | 89, 90, 93 | mp2b 10 |
. . . . . . . . . 10
⊢ (ω
⊆ (card‘𝑦)
↔ ¬ (card‘𝑦)
∈ ω) |
95 | 88, 94 | sylibr 226 |
. . . . . . . . 9
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦)) |
96 | 2, 95 | syl3an2b 1527 |
. . . . . . . 8
⊢ ((Lim
𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦)) |
97 | 96 | 3expb 1153 |
. . . . . . 7
⊢ ((Lim
𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦)) |
98 | 1, 97 | sylan2b 587 |
. . . . . 6
⊢ ((Lim
𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦)) |
99 | 98 | ralrimiva 3175 |
. . . . 5
⊢ (Lim
𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦)) |
100 | | ssiin 4790 |
. . . . 5
⊢ (ω
⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦)) |
101 | 99, 100 | sylibr 226 |
. . . 4
⊢ (Lim
𝐴 → ω ⊆
∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦)) |
102 | | cflim2.1 |
. . . . 5
⊢ 𝐴 ∈ V |
103 | 102 | cflim3 9399 |
. . . 4
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦)) |
104 | 101, 103 | sseqtr4d 3867 |
. . 3
⊢ (Lim
𝐴 → ω ⊆
(cf‘𝐴)) |
105 | | fvex 6446 |
. . . . . . 7
⊢
(card‘𝑦)
∈ V |
106 | 105 | dfiin2 4775 |
. . . . . 6
⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} |
107 | 103, 106 | syl6eq 2877 |
. . . . 5
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩
{𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}) |
108 | | cardlim 9111 |
. . . . . . . . 9
⊢ (ω
⊆ (card‘𝑦)
↔ Lim (card‘𝑦)) |
109 | | sseq2 3852 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆
(card‘𝑦))) |
110 | | limeq 5975 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦))) |
111 | 109, 110 | bibi12d 337 |
. . . . . . . . 9
⊢ (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦)))) |
112 | 108, 111 | mpbiri 250 |
. . . . . . . 8
⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥)) |
113 | 112 | rexlimivw 3238 |
. . . . . . 7
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥)) |
114 | 113 | ss2abi 3899 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} |
115 | | eleq1 2894 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On)) |
116 | 89, 115 | mpbiri 250 |
. . . . . . . . 9
⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
117 | 116 | rexlimivw 3238 |
. . . . . . . 8
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
118 | 117 | abssi 3902 |
. . . . . . 7
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On |
119 | | fvex 6446 |
. . . . . . . . 9
⊢
(cf‘𝐴) ∈
V |
120 | 107, 119 | syl6eqelr 2915 |
. . . . . . . 8
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ V) |
121 | | intex 5042 |
. . . . . . . 8
⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ V) |
122 | 120, 121 | sylibr 226 |
. . . . . . 7
⊢ (Lim
𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) |
123 | | onint 7256 |
. . . . . . 7
⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}) |
124 | 118, 122,
123 | sylancr 581 |
. . . . . 6
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}) |
125 | 114, 124 | sseldi 3825 |
. . . . 5
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}) |
126 | 107, 125 | eqeltrd 2906 |
. . . 4
⊢ (Lim
𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}) |
127 | | sseq2 3852 |
. . . . . 6
⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴))) |
128 | | limeq 5975 |
. . . . . 6
⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴))) |
129 | 127, 128 | bibi12d 337 |
. . . . 5
⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))) |
130 | 119, 129 | elab 3571 |
. . . 4
⊢
((cf‘𝐴) ∈
{𝑥 ∣ (ω ⊆
𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆
(cf‘𝐴) ↔ Lim
(cf‘𝐴))) |
131 | 126, 130 | sylib 210 |
. . 3
⊢ (Lim
𝐴 → (ω ⊆
(cf‘𝐴) ↔ Lim
(cf‘𝐴))) |
132 | 104, 131 | mpbid 224 |
. 2
⊢ (Lim
𝐴 → Lim
(cf‘𝐴)) |
133 | | eloni 5973 |
. . . . . . 7
⊢ (𝐴 ∈ On → Ord 𝐴) |
134 | | ordzsl 7306 |
. . . . . . 7
⊢ (Ord
𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
135 | 133, 134 | sylib 210 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
136 | | df-3or 1112 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴)) |
137 | | orcom 901 |
. . . . . . 7
⊢ (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
138 | | df-or 879 |
. . . . . . 7
⊢ ((Lim
𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
139 | 136, 137,
138 | 3bitri 289 |
. . . . . 6
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
140 | 135, 139 | sylib 210 |
. . . . 5
⊢ (𝐴 ∈ On → (¬ Lim
𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
141 | | fveq2 6433 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
(cf‘∅)) |
142 | | cf0 9388 |
. . . . . . . . 9
⊢
(cf‘∅) = ∅ |
143 | 141, 142 | syl6eq 2877 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
∅) |
144 | | limeq 5975 |
. . . . . . . 8
⊢
((cf‘𝐴) =
∅ → (Lim (cf‘𝐴) ↔ Lim ∅)) |
145 | 143, 144 | syl 17 |
. . . . . . 7
⊢ (𝐴 = ∅ → (Lim
(cf‘𝐴) ↔ Lim
∅)) |
146 | 78, 145 | mtbiri 319 |
. . . . . 6
⊢ (𝐴 = ∅ → ¬ Lim
(cf‘𝐴)) |
147 | | 1n0 7842 |
. . . . . . . . . 10
⊢
1o ≠ ∅ |
148 | | df1o2 7839 |
. . . . . . . . . . . 12
⊢
1o = {∅} |
149 | 148 | unieqi 4667 |
. . . . . . . . . . 11
⊢ ∪ 1o = ∪
{∅} |
150 | | 0ex 5014 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
151 | 150 | unisn 4674 |
. . . . . . . . . . 11
⊢ ∪ {∅} = ∅ |
152 | 149, 151 | eqtri 2849 |
. . . . . . . . . 10
⊢ ∪ 1o = ∅ |
153 | 147, 152 | neeqtrri 3072 |
. . . . . . . . 9
⊢
1o ≠ ∪
1o |
154 | | limuni 6023 |
. . . . . . . . . 10
⊢ (Lim
1o → 1o = ∪
1o) |
155 | 154 | necon3ai 3024 |
. . . . . . . . 9
⊢
(1o ≠ ∪ 1o →
¬ Lim 1o) |
156 | 153, 155 | ax-mp 5 |
. . . . . . . 8
⊢ ¬
Lim 1o |
157 | | fveq2 6433 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥)) |
158 | | cfsuc 9394 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → (cf‘suc
𝑥) =
1o) |
159 | 157, 158 | sylan9eqr 2883 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1o) |
160 | | limeq 5975 |
. . . . . . . . 9
⊢
((cf‘𝐴) =
1o → (Lim (cf‘𝐴) ↔ Lim
1o)) |
161 | 159, 160 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim
1o)) |
162 | 156, 161 | mtbiri 319 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴)) |
163 | 162 | rexlimiva 3237 |
. . . . . 6
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴)) |
164 | 146, 163 | jaoi 888 |
. . . . 5
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴)) |
165 | 140, 164 | syl6 35 |
. . . 4
⊢ (𝐴 ∈ On → (¬ Lim
𝐴 → ¬ Lim
(cf‘𝐴))) |
166 | 165 | con4d 115 |
. . 3
⊢ (𝐴 ∈ On → (Lim
(cf‘𝐴) → Lim
𝐴)) |
167 | | cff 9385 |
. . . . . . . . 9
⊢
cf:On⟶On |
168 | 167 | fdmi 6288 |
. . . . . . . 8
⊢ dom cf =
On |
169 | 168 | eleq2i 2898 |
. . . . . . 7
⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On) |
170 | | ndmfv 6463 |
. . . . . . 7
⊢ (¬
𝐴 ∈ dom cf →
(cf‘𝐴) =
∅) |
171 | 169, 170 | sylnbir 323 |
. . . . . 6
⊢ (¬
𝐴 ∈ On →
(cf‘𝐴) =
∅) |
172 | 171, 144 | syl 17 |
. . . . 5
⊢ (¬
𝐴 ∈ On → (Lim
(cf‘𝐴) ↔ Lim
∅)) |
173 | 78, 172 | mtbiri 319 |
. . . 4
⊢ (¬
𝐴 ∈ On → ¬
Lim (cf‘𝐴)) |
174 | 173 | pm2.21d 119 |
. . 3
⊢ (¬
𝐴 ∈ On → (Lim
(cf‘𝐴) → Lim
𝐴)) |
175 | 166, 174 | pm2.61i 177 |
. 2
⊢ (Lim
(cf‘𝐴) → Lim
𝐴) |
176 | 132, 175 | impbii 201 |
1
⊢ (Lim
𝐴 ↔ Lim
(cf‘𝐴)) |