Step | Hyp | Ref
| Expression |
1 | | pm3.24 393 |
. . . . . . 7
⊢ ¬
((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝑏 ∈ 𝑧 → ¬ ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin)) |
3 | 2 | nrex 3181 |
. . . . 5
⊢ ¬
∃𝑏 ∈ 𝑧 ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
4 | | r19.29 3258 |
. . . . 5
⊢
((∀𝑏 ∈
𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) → ∃𝑏 ∈ 𝑧 ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin)) |
5 | 3, 4 | mto 189 |
. . . 4
⊢ ¬
(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) → ¬
(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)) |
7 | 6 | nrex 3181 |
. 2
⊢ ¬
∃𝑧 ∈ (𝒫
𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
8 | | ralnex 3174 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴)) |
9 | | cmptop 21607 |
. . . . . . 7
⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top) |
10 | | bwt2.1 |
. . . . . . . . . . 11
⊢ 𝑋 = ∪
𝐽 |
11 | 10 | islp3 21358 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))) |
12 | 11 | 3expa 1108 |
. . . . . . . . 9
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))) |
13 | 12 | notbid 310 |
. . . . . . . 8
⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))) |
14 | 13 | ralbidva 3167 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∀𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))) |
15 | 9, 14 | sylan 575 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (∀𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))) |
16 | 8, 15 | syl5bbr 277 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))) |
17 | | rexanali 3179 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
𝐽 (𝑥 ∈ 𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) ↔ ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)) |
18 | | nne 2973 |
. . . . . . . . . . . 12
⊢ (¬
(𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅ ↔ (𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅) |
19 | | vex 3401 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
20 | | sneq 4408 |
. . . . . . . . . . . . . . . 16
⊢ (𝑜 = 𝑥 → {𝑜} = {𝑥}) |
21 | 20 | difeq2d 3951 |
. . . . . . . . . . . . . . 15
⊢ (𝑜 = 𝑥 → (𝐴 ∖ {𝑜}) = (𝐴 ∖ {𝑥})) |
22 | 21 | ineq2d 4037 |
. . . . . . . . . . . . . 14
⊢ (𝑜 = 𝑥 → (𝑏 ∩ (𝐴 ∖ {𝑜})) = (𝑏 ∩ (𝐴 ∖ {𝑥}))) |
23 | 22 | eqeq1d 2780 |
. . . . . . . . . . . . 13
⊢ (𝑜 = 𝑥 → ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ ↔ (𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅)) |
24 | 19, 23 | spcev 3502 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅ → ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) |
25 | 18, 24 | sylbi 209 |
. . . . . . . . . . 11
⊢ (¬
(𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅ → ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) |
26 | 25 | anim2i 610 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) |
27 | 26 | reximi 3192 |
. . . . . . . . 9
⊢
(∃𝑏 ∈
𝐽 (𝑥 ∈ 𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) |
28 | 17, 27 | sylbir 227 |
. . . . . . . 8
⊢ (¬
∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) |
29 | 28 | ralimi 3134 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∀𝑥 ∈ 𝑋 ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) |
30 | 10 | cmpcov2 21602 |
. . . . . . . 8
⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) |
31 | 30 | ex 403 |
. . . . . . 7
⊢ (𝐽 ∈ Comp →
(∀𝑥 ∈ 𝑋 ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))) |
32 | 29, 31 | syl5 34 |
. . . . . 6
⊢ (𝐽 ∈ Comp →
(∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))) |
33 | 32 | adantr 474 |
. . . . 5
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))) |
34 | 16, 33 | sylbid 232 |
. . . 4
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))) |
35 | 34 | 3adant3 1123 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))) |
36 | | inss2 4054 |
. . . . . . . . 9
⊢
(𝒫 𝐽 ∩
Fin) ⊆ Fin |
37 | 36 | sseli 3817 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) → 𝑧 ∈ Fin) |
38 | | sseq2 3846 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∪
𝑧 → (𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝑧)) |
39 | 38 | biimpac 472 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 = ∪ 𝑧) → 𝐴 ⊆ ∪ 𝑧) |
40 | | infssuni 8545 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝑧)
→ ∃𝑏 ∈
𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
41 | 40 | 3expa 1108 |
. . . . . . . . . . . 12
⊢ (((¬
𝐴 ∈ Fin ∧ 𝑧 ∈ Fin) ∧ 𝐴 ⊆ ∪ 𝑧)
→ ∃𝑏 ∈
𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
42 | 41 | ancoms 452 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ∪ 𝑧
∧ (¬ 𝐴 ∈ Fin
∧ 𝑧 ∈ Fin)) →
∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
43 | 39, 42 | sylan 575 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ 𝑋 ∧ 𝑋 = ∪ 𝑧) ∧ (¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
44 | 43 | an42s 651 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ (𝑧 ∈ Fin ∧ 𝑋 = ∪ 𝑧)) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
45 | 44 | anassrs 461 |
. . . . . . . 8
⊢ ((((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ Fin) ∧ 𝑋 = ∪ 𝑧) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
46 | 37, 45 | sylanl2 671 |
. . . . . . 7
⊢ ((((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = ∪ 𝑧) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) |
47 | | 0fin 8476 |
. . . . . . . . . . . 12
⊢ ∅
∈ Fin |
48 | | eleq1 2847 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin ↔ ∅ ∈
Fin)) |
49 | 47, 48 | mpbiri 250 |
. . . . . . . . . . 11
⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin) |
50 | | snfi 8326 |
. . . . . . . . . . 11
⊢ {𝑜} ∈ Fin |
51 | | unfi 8515 |
. . . . . . . . . . 11
⊢ (((𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin ∧ {𝑜} ∈ Fin) → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin) |
52 | 49, 50, 51 | sylancl 580 |
. . . . . . . . . 10
⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin) |
53 | | ssun1 3999 |
. . . . . . . . . . . 12
⊢ 𝑏 ⊆ (𝑏 ∪ {𝑜}) |
54 | | ssun1 3999 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑜}) |
55 | | undif1 4267 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ {𝑜}) ∪ {𝑜}) = (𝐴 ∪ {𝑜}) |
56 | 54, 55 | sseqtr4i 3857 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆ ((𝐴 ∖ {𝑜}) ∪ {𝑜}) |
57 | | ss2in 4061 |
. . . . . . . . . . . 12
⊢ ((𝑏 ⊆ (𝑏 ∪ {𝑜}) ∧ 𝐴 ⊆ ((𝐴 ∖ {𝑜}) ∪ {𝑜})) → (𝑏 ∩ 𝐴) ⊆ ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜}))) |
58 | 53, 56, 57 | mp2an 682 |
. . . . . . . . . . 11
⊢ (𝑏 ∩ 𝐴) ⊆ ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜})) |
59 | | incom 4028 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ 𝑏) = (𝑏 ∩ 𝐴) |
60 | | undir 4103 |
. . . . . . . . . . 11
⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) = ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜})) |
61 | 58, 59, 60 | 3sstr4i 3863 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝑏) ⊆ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) |
62 | | ssfi 8468 |
. . . . . . . . . 10
⊢ ((((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin ∧ (𝐴 ∩ 𝑏) ⊆ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜})) → (𝐴 ∩ 𝑏) ∈ Fin) |
63 | 52, 61, 62 | sylancl 580 |
. . . . . . . . 9
⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝐴 ∩ 𝑏) ∈ Fin) |
64 | 63 | exlimiv 1973 |
. . . . . . . 8
⊢
(∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝐴 ∩ 𝑏) ∈ Fin) |
65 | 64 | ralimi 3134 |
. . . . . . 7
⊢
(∀𝑏 ∈
𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin) |
66 | 46, 65 | anim12ci 607 |
. . . . . 6
⊢
(((((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = ∪ 𝑧) ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → (∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)) |
67 | 66 | expl 451 |
. . . . 5
⊢ (((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) → ((𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → (∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin))) |
68 | 67 | reximdva 3198 |
. . . 4
⊢ ((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin))) |
69 | 68 | 3adant1 1121 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin))) |
70 | 35, 69 | syld 47 |
. 2
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin))) |
71 | 7, 70 | mt3i 144 |
1
⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴)) |