Step |
Hyp |
Ref |
Expression |
1 |
|
bwt2.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
pm3.24 |
⊢ ¬ ( ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
3 |
2
|
a1i |
⊢ ( 𝑏 ∈ 𝑧 → ¬ ( ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) |
4 |
3
|
nrex |
⊢ ¬ ∃ 𝑏 ∈ 𝑧 ( ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
5 |
|
r19.29 |
⊢ ( ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) → ∃ 𝑏 ∈ 𝑧 ( ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) |
6 |
4 5
|
mto |
⊢ ¬ ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
7 |
6
|
a1i |
⊢ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) → ¬ ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) |
8 |
7
|
nrex |
⊢ ¬ ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
9 |
|
ralnex |
⊢ ( ∀ 𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ) |
10 |
|
cmptop |
⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top ) |
11 |
1
|
islp3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) ) |
12 |
11
|
3expa |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) ) |
13 |
12
|
notbid |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ¬ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) ) |
14 |
13
|
ralbidva |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) ) |
15 |
10 14
|
sylan |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) ) |
16 |
9 15
|
bitr3id |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) ) |
17 |
|
rexanali |
⊢ ( ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ¬ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ↔ ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) ) |
18 |
|
nne |
⊢ ( ¬ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ↔ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ ) |
19 |
|
vex |
⊢ 𝑥 ∈ V |
20 |
|
sneq |
⊢ ( 𝑜 = 𝑥 → { 𝑜 } = { 𝑥 } ) |
21 |
20
|
difeq2d |
⊢ ( 𝑜 = 𝑥 → ( 𝐴 ∖ { 𝑜 } ) = ( 𝐴 ∖ { 𝑥 } ) ) |
22 |
21
|
ineq2d |
⊢ ( 𝑜 = 𝑥 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ) |
23 |
22
|
eqeq1d |
⊢ ( 𝑜 = 𝑥 → ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ↔ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ ) ) |
24 |
19 23
|
spcev |
⊢ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) = ∅ → ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) |
25 |
18 24
|
sylbi |
⊢ ( ¬ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ → ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) |
26 |
25
|
anim2i |
⊢ ( ( 𝑥 ∈ 𝑏 ∧ ¬ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) → ( 𝑥 ∈ 𝑏 ∧ ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) |
27 |
26
|
reximi |
⊢ ( ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ¬ ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) → ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) |
28 |
17 27
|
sylbir |
⊢ ( ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) → ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) |
29 |
28
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) → ∀ 𝑥 ∈ 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) |
30 |
1
|
cmpcov2 |
⊢ ( ( 𝐽 ∈ Comp ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) |
31 |
30
|
ex |
⊢ ( 𝐽 ∈ Comp → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 ∧ ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) ) |
32 |
29 31
|
syl5 |
⊢ ( 𝐽 ∈ Comp → ( ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) ) |
33 |
32
|
adantr |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ¬ ∀ 𝑏 ∈ 𝐽 ( 𝑥 ∈ 𝑏 → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑥 } ) ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) ) |
34 |
16 33
|
sylbid |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) ) |
35 |
34
|
3adant3 |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) ) ) |
36 |
|
elinel2 |
⊢ ( 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) → 𝑧 ∈ Fin ) |
37 |
|
sseq2 |
⊢ ( 𝑋 = ∪ 𝑧 → ( 𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝑧 ) ) |
38 |
37
|
biimpac |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 = ∪ 𝑧 ) → 𝐴 ⊆ ∪ 𝑧 ) |
39 |
|
infssuni |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝑧 ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
40 |
39
|
3expa |
⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ) ∧ 𝐴 ⊆ ∪ 𝑧 ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
41 |
40
|
ancoms |
⊢ ( ( 𝐴 ⊆ ∪ 𝑧 ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ) ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
42 |
38 41
|
sylan |
⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ 𝑋 = ∪ 𝑧 ) ∧ ( ¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ) ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
43 |
42
|
an42s |
⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ ( 𝑧 ∈ Fin ∧ 𝑋 = ∪ 𝑧 ) ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
44 |
43
|
anassrs |
⊢ ( ( ( ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ∈ Fin ) ∧ 𝑋 = ∪ 𝑧 ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
45 |
36 44
|
sylanl2 |
⊢ ( ( ( ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ) ∧ 𝑋 = ∪ 𝑧 ) → ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
46 |
|
0fin |
⊢ ∅ ∈ Fin |
47 |
|
eleq1 |
⊢ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ → ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∈ Fin ↔ ∅ ∈ Fin ) ) |
48 |
46 47
|
mpbiri |
⊢ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ → ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∈ Fin ) |
49 |
|
snfi |
⊢ { 𝑜 } ∈ Fin |
50 |
|
unfi |
⊢ ( ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∈ Fin ∧ { 𝑜 } ∈ Fin ) → ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∪ { 𝑜 } ) ∈ Fin ) |
51 |
48 49 50
|
sylancl |
⊢ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ → ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∪ { 𝑜 } ) ∈ Fin ) |
52 |
|
ssun1 |
⊢ 𝑏 ⊆ ( 𝑏 ∪ { 𝑜 } ) |
53 |
|
ssun1 |
⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑜 } ) |
54 |
|
undif1 |
⊢ ( ( 𝐴 ∖ { 𝑜 } ) ∪ { 𝑜 } ) = ( 𝐴 ∪ { 𝑜 } ) |
55 |
53 54
|
sseqtrri |
⊢ 𝐴 ⊆ ( ( 𝐴 ∖ { 𝑜 } ) ∪ { 𝑜 } ) |
56 |
|
ss2in |
⊢ ( ( 𝑏 ⊆ ( 𝑏 ∪ { 𝑜 } ) ∧ 𝐴 ⊆ ( ( 𝐴 ∖ { 𝑜 } ) ∪ { 𝑜 } ) ) → ( 𝑏 ∩ 𝐴 ) ⊆ ( ( 𝑏 ∪ { 𝑜 } ) ∩ ( ( 𝐴 ∖ { 𝑜 } ) ∪ { 𝑜 } ) ) ) |
57 |
52 55 56
|
mp2an |
⊢ ( 𝑏 ∩ 𝐴 ) ⊆ ( ( 𝑏 ∪ { 𝑜 } ) ∩ ( ( 𝐴 ∖ { 𝑜 } ) ∪ { 𝑜 } ) ) |
58 |
|
incom |
⊢ ( 𝐴 ∩ 𝑏 ) = ( 𝑏 ∩ 𝐴 ) |
59 |
|
undir |
⊢ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∪ { 𝑜 } ) = ( ( 𝑏 ∪ { 𝑜 } ) ∩ ( ( 𝐴 ∖ { 𝑜 } ) ∪ { 𝑜 } ) ) |
60 |
57 58 59
|
3sstr4i |
⊢ ( 𝐴 ∩ 𝑏 ) ⊆ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∪ { 𝑜 } ) |
61 |
|
ssfi |
⊢ ( ( ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∪ { 𝑜 } ) ∈ Fin ∧ ( 𝐴 ∩ 𝑏 ) ⊆ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) ∪ { 𝑜 } ) ) → ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
62 |
51 60 61
|
sylancl |
⊢ ( ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ → ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
63 |
62
|
exlimiv |
⊢ ( ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ → ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
64 |
63
|
ralimi |
⊢ ( ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ → ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ) |
65 |
45 64
|
anim12ci |
⊢ ( ( ( ( ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ) ∧ 𝑋 = ∪ 𝑧 ) ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) → ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) |
66 |
65
|
expl |
⊢ ( ( ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ) → ( ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) → ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) ) |
67 |
66
|
reximdva |
⊢ ( ( 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) ) |
68 |
67
|
3adant1 |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( 𝑋 = ∪ 𝑧 ∧ ∀ 𝑏 ∈ 𝑧 ∃ 𝑜 ( 𝑏 ∩ ( 𝐴 ∖ { 𝑜 } ) ) = ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) ) |
69 |
35 68
|
syld |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ( ¬ ∃ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) → ∃ 𝑧 ∈ ( 𝒫 𝐽 ∩ Fin ) ( ∀ 𝑏 ∈ 𝑧 ( 𝐴 ∩ 𝑏 ) ∈ Fin ∧ ∃ 𝑏 ∈ 𝑧 ¬ ( 𝐴 ∩ 𝑏 ) ∈ Fin ) ) ) |
70 |
8 69
|
mt3i |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) ) |