Step | Hyp | Ref
| Expression |
1 | | rabid 3095 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) |
2 | | selpw 4115 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
3 | | limord 5701 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Lim
𝐴 → Ord 𝐴) |
4 | | ordsson 6881 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Ord
𝐴 → 𝐴 ⊆ On) |
5 | | sstr 3576 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On) → 𝑦 ⊆ On) |
6 | 5 | expcom 450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴 ⊆ On → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On)) |
7 | 3, 4, 6 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Lim
𝐴 → (𝑦 ⊆ 𝐴 → 𝑦 ⊆ On)) |
8 | 7 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴) → 𝑦 ⊆ On) |
9 | 8 | 3adant3 1074 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ⊆ On) |
10 | | ssel2 3563 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → 𝑠 ∈ On) |
11 | | eloni 5650 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ On → Ord 𝑠) |
12 | | ordirr 5658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑠 → ¬ 𝑠 ∈ 𝑠) |
13 | 10, 11, 12 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑠 ∈ 𝑠) |
14 | | ssel 3562 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ⊆ 𝑠 → (𝑠 ∈ 𝑦 → 𝑠 ∈ 𝑠)) |
15 | 14 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ 𝑦 → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠)) |
16 | 15 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (𝑦 ⊆ 𝑠 → 𝑠 ∈ 𝑠)) |
17 | 13, 16 | mtod 188 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠) |
18 | 9, 17 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝑦 ⊆ 𝑠) |
19 | | simpl2 1058 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → 𝑦 ⊆ 𝐴) |
20 | | sstr 3576 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠) |
21 | 19, 20 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) ∧ 𝐴 ⊆ 𝑠) → 𝑦 ⊆ 𝑠) |
22 | 18, 21 | mtand 689 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ 𝐴 ⊆ 𝑠) |
23 | | simpl3 1059 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ∪ 𝑦 = 𝐴) |
24 | 23 | sseq1d 3595 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → (∪ 𝑦 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠)) |
25 | 22, 24 | mtbird 314 |
. . . . . . . . . . . . . 14
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∪
𝑦 ⊆ 𝑠) |
26 | | unissb 4405 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑦
⊆ 𝑠 ↔
∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠) |
27 | 25, 26 | sylnib 317 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ 𝑠 ∈ 𝑦) → ¬ ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠) |
28 | 27 | nrexdv 2984 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠) |
29 | | ssel 3562 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → (𝑠 ∈ 𝑦 → 𝑠 ∈ On)) |
30 | | ssel 3562 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → (𝑡 ∈ 𝑦 → 𝑡 ∈ On)) |
31 | | ontri1 5674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 ∈ On ∧ 𝑠 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)) |
32 | 31 | ancoms 468 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑠 ∈ 𝑡)) |
33 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑡 ∈ V |
34 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑠 ∈ V |
35 | 33, 34 | brcnv 5227 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡◡ E 𝑠 ↔ 𝑠 E 𝑡) |
36 | | epel 4952 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 E 𝑡 ↔ 𝑠 ∈ 𝑡) |
37 | 35, 36 | bitri 263 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡◡ E 𝑠 ↔ 𝑠 ∈ 𝑡) |
38 | 37 | notbii 309 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑡◡ E 𝑠 ↔ ¬ 𝑠 ∈ 𝑡) |
39 | 32, 38 | syl6bbr 277 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠)) |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → ((𝑠 ∈ On ∧ 𝑡 ∈ On) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠))) |
41 | 29, 30, 40 | syl2and 499 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ On → ((𝑠 ∈ 𝑦 ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠))) |
42 | 41 | impl 648 |
. . . . . . . . . . . . . . 15
⊢ (((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) ∧ 𝑡 ∈ 𝑦) → (𝑡 ⊆ 𝑠 ↔ ¬ 𝑡◡ E
𝑠)) |
43 | 42 | ralbidva 2968 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ On ∧ 𝑠 ∈ 𝑦) → (∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠)) |
44 | 43 | rexbidva 3031 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ On → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠)) |
45 | 9, 44 | syl 17 |
. . . . . . . . . . . 12
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → (∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 𝑡 ⊆ 𝑠 ↔ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠)) |
46 | 28, 45 | mtbid 313 |
. . . . . . . . . . 11
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠) |
47 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
48 | 47 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ∈ V) |
49 | | epweon 6875 |
. . . . . . . . . . . . . . . . . . 19
⊢ E We
On |
50 | | wess 5025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ⊆ On → ( E We On
→ E We 𝑦)) |
51 | 49, 50 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ⊆ On → E We 𝑦) |
52 | | weso 5029 |
. . . . . . . . . . . . . . . . . 18
⊢ ( E We
𝑦 → E Or 𝑦) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → E Or 𝑦) |
54 | | cnvso 5591 |
. . . . . . . . . . . . . . . . 17
⊢ ( E Or
𝑦 ↔ ◡ E Or 𝑦) |
55 | 53, 54 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ⊆ On → ◡ E Or 𝑦) |
56 | 55 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → ◡ E Or 𝑦) |
57 | | onssnum 8746 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ V ∧ 𝑦 ⊆ On) → 𝑦 ∈ dom
card) |
58 | 47, 57 | mpan 702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ⊆ On → 𝑦 ∈ dom
card) |
59 | | cardid2 8662 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ dom card →
(card‘𝑦) ≈
𝑦) |
60 | | ensym 7891 |
. . . . . . . . . . . . . . . . . 18
⊢
((card‘𝑦)
≈ 𝑦 → 𝑦 ≈ (card‘𝑦)) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ⊆ On → 𝑦 ≈ (card‘𝑦)) |
62 | | nnsdom 8434 |
. . . . . . . . . . . . . . . . 17
⊢
((card‘𝑦)
∈ ω → (card‘𝑦) ≺ ω) |
63 | | ensdomtr 7981 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ≈ (card‘𝑦) ∧ (card‘𝑦) ≺ ω) → 𝑦 ≺
ω) |
64 | 61, 62, 63 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → 𝑦 ≺
ω) |
65 | | isfinite 8432 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ Fin ↔ 𝑦 ≺
ω) |
66 | 64, 65 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → 𝑦 ∈
Fin) |
67 | | wofi 8094 |
. . . . . . . . . . . . . . 15
⊢ ((◡ E Or 𝑦 ∧ 𝑦 ∈ Fin) → ◡ E We 𝑦) |
68 | 56, 66, 67 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ On ∧
(card‘𝑦) ∈
ω) → ◡ E We 𝑦) |
69 | 9, 68 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E We 𝑦) |
70 | | wefr 5028 |
. . . . . . . . . . . . 13
⊢ (◡ E We 𝑦 → ◡ E Fr 𝑦) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ◡ E Fr 𝑦) |
72 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ 𝑦 ⊆ 𝑦 |
73 | 72 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ⊆ 𝑦) |
74 | | unieq 4380 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∪ ∅) |
75 | | uni0 4401 |
. . . . . . . . . . . . . . . . . . 19
⊢ ∪ ∅ = ∅ |
76 | 74, 75 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∅) |
77 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (∪ 𝑦 =
𝐴 → (∪ 𝑦 =
∅ ↔ 𝐴 =
∅)) |
78 | 76, 77 | syl5ib 233 |
. . . . . . . . . . . . . . . . 17
⊢ (∪ 𝑦 =
𝐴 → (𝑦 = ∅ → 𝐴 = ∅)) |
79 | | nlim0 5700 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
Lim ∅ |
80 | | limeq 5652 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 = ∅ → (Lim 𝐴 ↔ Lim
∅)) |
81 | 79, 80 | mtbiri 316 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 = ∅ → ¬ Lim
𝐴) |
82 | 78, 81 | syl6 34 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑦 =
𝐴 → (𝑦 = ∅ → ¬ Lim
𝐴)) |
83 | 82 | necon2ad 2797 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑦 =
𝐴 → (Lim 𝐴 → 𝑦 ≠ ∅)) |
84 | 83 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝐴 ∧ ∪ 𝑦 =
𝐴) → 𝑦 ≠ ∅) |
85 | 84 | 3adant2 1073 |
. . . . . . . . . . . . 13
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → 𝑦 ≠ ∅) |
86 | 85 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → 𝑦 ≠ ∅) |
87 | | fri 5000 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ V ∧ ◡ E Fr 𝑦) ∧ (𝑦 ⊆ 𝑦 ∧ 𝑦 ≠ ∅)) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠) |
88 | 48, 71, 73, 86, 87 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) ∧ (card‘𝑦) ∈ ω) → ∃𝑠 ∈ 𝑦 ∀𝑡 ∈ 𝑦 ¬ 𝑡◡ E
𝑠) |
89 | 46, 88 | mtand 689 |
. . . . . . . . . 10
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ¬ (card‘𝑦) ∈
ω) |
90 | | cardon 8653 |
. . . . . . . . . . 11
⊢
(card‘𝑦)
∈ On |
91 | | eloni 5650 |
. . . . . . . . . . 11
⊢
((card‘𝑦)
∈ On → Ord (card‘𝑦)) |
92 | | ordom 6966 |
. . . . . . . . . . . 12
⊢ Ord
ω |
93 | | ordtri1 5673 |
. . . . . . . . . . . 12
⊢ ((Ord
ω ∧ Ord (card‘𝑦)) → (ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈
ω)) |
94 | 92, 93 | mpan 702 |
. . . . . . . . . . 11
⊢ (Ord
(card‘𝑦) →
(ω ⊆ (card‘𝑦) ↔ ¬ (card‘𝑦) ∈ ω)) |
95 | 90, 91, 94 | mp2b 10 |
. . . . . . . . . 10
⊢ (ω
⊆ (card‘𝑦)
↔ ¬ (card‘𝑦)
∈ ω) |
96 | 89, 95 | sylibr 223 |
. . . . . . . . 9
⊢ ((Lim
𝐴 ∧ 𝑦 ⊆ 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦)) |
97 | 2, 96 | syl3an2b 1355 |
. . . . . . . 8
⊢ ((Lim
𝐴 ∧ 𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴) → ω ⊆ (card‘𝑦)) |
98 | 97 | 3expb 1258 |
. . . . . . 7
⊢ ((Lim
𝐴 ∧ (𝑦 ∈ 𝒫 𝐴 ∧ ∪ 𝑦 = 𝐴)) → ω ⊆ (card‘𝑦)) |
99 | 1, 98 | sylan2b 491 |
. . . . . 6
⊢ ((Lim
𝐴 ∧ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}) → ω ⊆ (card‘𝑦)) |
100 | 99 | ralrimiva 2949 |
. . . . 5
⊢ (Lim
𝐴 → ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦)) |
101 | | ssiin 4506 |
. . . . 5
⊢ (ω
⊆ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) ↔ ∀𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}ω ⊆ (card‘𝑦)) |
102 | 100, 101 | sylibr 223 |
. . . 4
⊢ (Lim
𝐴 → ω ⊆
∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦)) |
103 | | cflim2.1 |
. . . . 5
⊢ 𝐴 ∈ V |
104 | 103 | cflim3 8967 |
. . . 4
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦)) |
105 | 102, 104 | sseqtr4d 3605 |
. . 3
⊢ (Lim
𝐴 → ω ⊆
(cf‘𝐴)) |
106 | | fvex 6113 |
. . . . . . 7
⊢
(card‘𝑦)
∈ V |
107 | 106 | dfiin2 4491 |
. . . . . 6
⊢ ∩ 𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴} (card‘𝑦) = ∩ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} |
108 | 104, 107 | syl6eq 2660 |
. . . . 5
⊢ (Lim
𝐴 → (cf‘𝐴) = ∩
{𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}) |
109 | | cardlim 8681 |
. . . . . . . . 9
⊢ (ω
⊆ (card‘𝑦)
↔ Lim (card‘𝑦)) |
110 | | sseq2 3590 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ ω ⊆
(card‘𝑦))) |
111 | | limeq 5652 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (Lim 𝑥 ↔ Lim (card‘𝑦))) |
112 | 110, 111 | bibi12d 334 |
. . . . . . . . 9
⊢ (𝑥 = (card‘𝑦) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (card‘𝑦) ↔ Lim (card‘𝑦)))) |
113 | 109, 112 | mpbiri 247 |
. . . . . . . 8
⊢ (𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥)) |
114 | 113 | rexlimivw 3011 |
. . . . . . 7
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦) → (ω ⊆ 𝑥 ↔ Lim 𝑥)) |
115 | 114 | ss2abi 3637 |
. . . . . 6
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)} |
116 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = (card‘𝑦) → (𝑥 ∈ On ↔ (card‘𝑦) ∈ On)) |
117 | 90, 116 | mpbiri 247 |
. . . . . . . . 9
⊢ (𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
118 | 117 | rexlimivw 3011 |
. . . . . . . 8
⊢
(∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦) → 𝑥 ∈ On) |
119 | 118 | abssi 3640 |
. . . . . . 7
⊢ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On |
120 | | fvex 6113 |
. . . . . . . . 9
⊢
(cf‘𝐴) ∈
V |
121 | 108, 120 | syl6eqelr 2697 |
. . . . . . . 8
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ V) |
122 | | intex 4747 |
. . . . . . . 8
⊢ ({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅ ↔ ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ V) |
123 | 121, 122 | sylibr 223 |
. . . . . . 7
⊢ (Lim
𝐴 → {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) |
124 | | onint 6887 |
. . . . . . 7
⊢ (({𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ⊆ On ∧ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)} ≠ ∅) → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}) |
125 | 119, 123,
124 | sylancr 694 |
. . . . . 6
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ ∃𝑦 ∈ {𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 = 𝐴}𝑥 = (card‘𝑦)}) |
126 | 115, 125 | sseldi 3566 |
. . . . 5
⊢ (Lim
𝐴 → ∩ {𝑥
∣ ∃𝑦 ∈
{𝑦 ∈ 𝒫 𝐴 ∣ ∪ 𝑦 =
𝐴}𝑥 = (card‘𝑦)} ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}) |
127 | 108, 126 | eqeltrd 2688 |
. . . 4
⊢ (Lim
𝐴 → (cf‘𝐴) ∈ {𝑥 ∣ (ω ⊆ 𝑥 ↔ Lim 𝑥)}) |
128 | | sseq2 3590 |
. . . . . 6
⊢ (𝑥 = (cf‘𝐴) → (ω ⊆ 𝑥 ↔ ω ⊆ (cf‘𝐴))) |
129 | | limeq 5652 |
. . . . . 6
⊢ (𝑥 = (cf‘𝐴) → (Lim 𝑥 ↔ Lim (cf‘𝐴))) |
130 | 128, 129 | bibi12d 334 |
. . . . 5
⊢ (𝑥 = (cf‘𝐴) → ((ω ⊆ 𝑥 ↔ Lim 𝑥) ↔ (ω ⊆ (cf‘𝐴) ↔ Lim (cf‘𝐴)))) |
131 | 120, 130 | elab 3319 |
. . . 4
⊢
((cf‘𝐴) ∈
{𝑥 ∣ (ω ⊆
𝑥 ↔ Lim 𝑥)} ↔ (ω ⊆
(cf‘𝐴) ↔ Lim
(cf‘𝐴))) |
132 | 127, 131 | sylib 207 |
. . 3
⊢ (Lim
𝐴 → (ω ⊆
(cf‘𝐴) ↔ Lim
(cf‘𝐴))) |
133 | 105, 132 | mpbid 221 |
. 2
⊢ (Lim
𝐴 → Lim
(cf‘𝐴)) |
134 | | eloni 5650 |
. . . . . . 7
⊢ (𝐴 ∈ On → Ord 𝐴) |
135 | | ordzsl 6937 |
. . . . . . 7
⊢ (Ord
𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
136 | 134, 135 | sylib 207 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
137 | | df-3or 1032 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴)) |
138 | | orcom 401 |
. . . . . . 7
⊢ (((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) ∨ Lim 𝐴) ↔ (Lim 𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
139 | | df-or 384 |
. . . . . . 7
⊢ ((Lim
𝐴 ∨ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
140 | 137, 138,
139 | 3bitri 285 |
. . . . . 6
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (¬ Lim 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
141 | 136, 140 | sylib 207 |
. . . . 5
⊢ (𝐴 ∈ On → (¬ Lim
𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥))) |
142 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
(cf‘∅)) |
143 | | cf0 8956 |
. . . . . . . . 9
⊢
(cf‘∅) = ∅ |
144 | 142, 143 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐴 = ∅ →
(cf‘𝐴) =
∅) |
145 | | limeq 5652 |
. . . . . . . 8
⊢
((cf‘𝐴) =
∅ → (Lim (cf‘𝐴) ↔ Lim ∅)) |
146 | 144, 145 | syl 17 |
. . . . . . 7
⊢ (𝐴 = ∅ → (Lim
(cf‘𝐴) ↔ Lim
∅)) |
147 | 79, 146 | mtbiri 316 |
. . . . . 6
⊢ (𝐴 = ∅ → ¬ Lim
(cf‘𝐴)) |
148 | | 1n0 7462 |
. . . . . . . . . 10
⊢
1𝑜 ≠ ∅ |
149 | | df1o2 7459 |
. . . . . . . . . . . 12
⊢
1𝑜 = {∅} |
150 | 149 | unieqi 4381 |
. . . . . . . . . . 11
⊢ ∪ 1𝑜 = ∪
{∅} |
151 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
152 | 151 | unisn 4387 |
. . . . . . . . . . 11
⊢ ∪ {∅} = ∅ |
153 | 150, 152 | eqtri 2632 |
. . . . . . . . . 10
⊢ ∪ 1𝑜 = ∅ |
154 | 148, 153 | neeqtrri 2855 |
. . . . . . . . 9
⊢
1𝑜 ≠ ∪
1𝑜 |
155 | | limuni 5702 |
. . . . . . . . . 10
⊢ (Lim
1𝑜 → 1𝑜 = ∪ 1𝑜) |
156 | 155 | necon3ai 2807 |
. . . . . . . . 9
⊢
(1𝑜 ≠ ∪
1𝑜 → ¬ Lim 1𝑜) |
157 | 154, 156 | ax-mp 5 |
. . . . . . . 8
⊢ ¬
Lim 1𝑜 |
158 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝐴 = suc 𝑥 → (cf‘𝐴) = (cf‘suc 𝑥)) |
159 | | cfsuc 8962 |
. . . . . . . . . 10
⊢ (𝑥 ∈ On → (cf‘suc
𝑥) =
1𝑜) |
160 | 158, 159 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (cf‘𝐴) = 1𝑜) |
161 | | limeq 5652 |
. . . . . . . . 9
⊢
((cf‘𝐴) =
1𝑜 → (Lim (cf‘𝐴) ↔ Lim
1𝑜)) |
162 | 160, 161 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → (Lim (cf‘𝐴) ↔ Lim
1𝑜)) |
163 | 157, 162 | mtbiri 316 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴)) |
164 | 163 | rexlimiva 3010 |
. . . . . 6
⊢
(∃𝑥 ∈ On
𝐴 = suc 𝑥 → ¬ Lim (cf‘𝐴)) |
165 | 147, 164 | jaoi 393 |
. . . . 5
⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥) → ¬ Lim (cf‘𝐴)) |
166 | 141, 165 | syl6 34 |
. . . 4
⊢ (𝐴 ∈ On → (¬ Lim
𝐴 → ¬ Lim
(cf‘𝐴))) |
167 | 166 | con4d 113 |
. . 3
⊢ (𝐴 ∈ On → (Lim
(cf‘𝐴) → Lim
𝐴)) |
168 | | cff 8953 |
. . . . . . . . 9
⊢
cf:On⟶On |
169 | 168 | fdmi 5965 |
. . . . . . . 8
⊢ dom cf =
On |
170 | 169 | eleq2i 2680 |
. . . . . . 7
⊢ (𝐴 ∈ dom cf ↔ 𝐴 ∈ On) |
171 | | ndmfv 6128 |
. . . . . . 7
⊢ (¬
𝐴 ∈ dom cf →
(cf‘𝐴) =
∅) |
172 | 170, 171 | sylnbir 320 |
. . . . . 6
⊢ (¬
𝐴 ∈ On →
(cf‘𝐴) =
∅) |
173 | 172, 145 | syl 17 |
. . . . 5
⊢ (¬
𝐴 ∈ On → (Lim
(cf‘𝐴) ↔ Lim
∅)) |
174 | 79, 173 | mtbiri 316 |
. . . 4
⊢ (¬
𝐴 ∈ On → ¬
Lim (cf‘𝐴)) |
175 | 174 | pm2.21d 117 |
. . 3
⊢ (¬
𝐴 ∈ On → (Lim
(cf‘𝐴) → Lim
𝐴)) |
176 | 167, 175 | pm2.61i 175 |
. 2
⊢ (Lim
(cf‘𝐴) → Lim
𝐴) |
177 | 133, 176 | impbii 198 |
1
⊢ (Lim
𝐴 ↔ Lim
(cf‘𝐴)) |