Step |
Hyp |
Ref |
Expression |
1 |
|
elpwi |
⊢ ( 𝑦 ∈ 𝒫 𝐽 → 𝑦 ⊆ 𝐽 ) |
2 |
|
0ss |
⊢ ∅ ⊆ 𝑦 |
3 |
|
0fin |
⊢ ∅ ∈ Fin |
4 |
|
elfpw |
⊢ ( ∅ ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( ∅ ⊆ 𝑦 ∧ ∅ ∈ Fin ) ) |
5 |
2 3 4
|
mpbir2an |
⊢ ∅ ∈ ( 𝒫 𝑦 ∩ Fin ) |
6 |
|
simprr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦 ) ) → ∪ 𝐽 = ∪ 𝑦 ) |
7 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦 ) ) → 𝑦 = ∅ ) |
8 |
7
|
unieqd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦 ) ) → ∪ 𝑦 = ∪ ∅ ) |
9 |
6 8
|
eqtrd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦 ) ) → ∪ 𝐽 = ∪ ∅ ) |
10 |
|
unieq |
⊢ ( 𝑧 = ∅ → ∪ 𝑧 = ∪ ∅ ) |
11 |
10
|
rspceeqv |
⊢ ( ( ∅ ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ ∪ 𝐽 = ∪ ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) |
12 |
5 9 11
|
sylancr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 = ∅ ∧ ∪ 𝐽 = ∪ 𝑦 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) |
13 |
12
|
expr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) |
14 |
|
vn0 |
⊢ V ≠ ∅ |
15 |
|
iineq1 |
⊢ ( 𝑦 = ∅ → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ 𝑟 ∈ ∅ ( ∪ 𝐽 ∖ 𝑟 ) ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ 𝑟 ∈ ∅ ( ∪ 𝐽 ∖ 𝑟 ) ) |
17 |
|
0iin |
⊢ ∩ 𝑟 ∈ ∅ ( ∪ 𝐽 ∖ 𝑟 ) = V |
18 |
16 17
|
eqtrdi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = V ) |
19 |
18
|
eqeq1d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ↔ V = ∅ ) ) |
20 |
19
|
necon3bbid |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ( ¬ ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ↔ V ≠ ∅ ) ) |
21 |
14 20
|
mpbiri |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ¬ ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ) |
22 |
21
|
pm2.21d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) |
23 |
13 22
|
2thd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 = ∅ ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) ) |
24 |
|
uniss |
⊢ ( 𝑦 ⊆ 𝐽 → ∪ 𝑦 ⊆ ∪ 𝐽 ) |
25 |
24
|
ad2antlr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ∪ 𝑦 ⊆ ∪ 𝐽 ) |
26 |
|
eqss |
⊢ ( ∪ 𝑦 = ∪ 𝐽 ↔ ( ∪ 𝑦 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑦 ) ) |
27 |
26
|
baib |
⊢ ( ∪ 𝑦 ⊆ ∪ 𝐽 → ( ∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦 ) ) |
28 |
25 27
|
syl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑦 ) ) |
29 |
|
eqcom |
⊢ ( ∪ 𝑦 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑦 ) |
30 |
|
ssdif0 |
⊢ ( ∪ 𝐽 ⊆ ∪ 𝑦 ↔ ( ∪ 𝐽 ∖ ∪ 𝑦 ) = ∅ ) |
31 |
28 29 30
|
3bitr3g |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∪ 𝐽 = ∪ 𝑦 ↔ ( ∪ 𝐽 ∖ ∪ 𝑦 ) = ∅ ) ) |
32 |
|
iindif2 |
⊢ ( 𝑦 ≠ ∅ → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟 ) ) |
33 |
32
|
adantl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟 ) ) |
34 |
|
uniiun |
⊢ ∪ 𝑦 = ∪ 𝑟 ∈ 𝑦 𝑟 |
35 |
34
|
difeq2i |
⊢ ( ∪ 𝐽 ∖ ∪ 𝑦 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑦 𝑟 ) |
36 |
33 35
|
eqtr4di |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ( ∪ 𝐽 ∖ ∪ 𝑦 ) ) |
37 |
36
|
eqeq1d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ↔ ( ∪ 𝐽 ∖ ∪ 𝑦 ) = ∅ ) ) |
38 |
31 37
|
bitr4d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∪ 𝐽 = ∪ 𝑦 ↔ ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ) ) |
39 |
|
imassrn |
⊢ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ⊆ ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) |
40 |
|
df-ima |
⊢ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ran ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑦 ) |
41 |
|
resmpt |
⊢ ( 𝑦 ⊆ 𝐽 → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑦 ) = ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
42 |
41
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑦 ) = ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
43 |
42
|
rneqd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ran ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑦 ) = ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
44 |
40 43
|
syl5eq |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
45 |
44
|
ad2antrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
46 |
39 45
|
sseqtrrid |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) |
47 |
|
funmpt |
⊢ Fun ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) |
48 |
|
elinel2 |
⊢ ( 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) → 𝑧 ∈ Fin ) |
49 |
48
|
adantl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) → 𝑧 ∈ Fin ) |
50 |
|
imafi |
⊢ ( ( Fun ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ∧ 𝑧 ∈ Fin ) → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ∈ Fin ) |
51 |
47 49 50
|
sylancr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ∈ Fin ) |
52 |
|
elfpw |
⊢ ( ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ↔ ( ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∧ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ∈ Fin ) ) |
53 |
46 51 52
|
sylanbrc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) |
54 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
55 |
54
|
topopn |
⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽 ) |
56 |
55
|
difexd |
⊢ ( 𝐽 ∈ Top → ( ∪ 𝐽 ∖ 𝑟 ) ∈ V ) |
57 |
56
|
ralrimivw |
⊢ ( 𝐽 ∈ Top → ∀ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V ) |
58 |
|
eqid |
⊢ ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) = ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) |
59 |
58
|
fnmpt |
⊢ ( ∀ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V → ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) Fn 𝑦 ) |
60 |
57 59
|
syl |
⊢ ( 𝐽 ∈ Top → ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) Fn 𝑦 ) |
61 |
60
|
ad3antrrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) Fn 𝑦 ) |
62 |
|
simpr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) |
63 |
|
elfpw |
⊢ ( 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ↔ ( 𝑤 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∧ 𝑤 ∈ Fin ) ) |
64 |
62 63
|
sylib |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → ( 𝑤 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∧ 𝑤 ∈ Fin ) ) |
65 |
64
|
simpld |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → 𝑤 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) |
66 |
44
|
ad2antrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
67 |
65 66
|
sseqtrd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → 𝑤 ⊆ ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
68 |
64
|
simprd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → 𝑤 ∈ Fin ) |
69 |
|
fipreima |
⊢ ( ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) Fn 𝑦 ∧ 𝑤 ⊆ ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ∧ 𝑤 ∈ Fin ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = 𝑤 ) |
70 |
61 67 68 69
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = 𝑤 ) |
71 |
|
eqcom |
⊢ ( ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = 𝑤 ↔ 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
72 |
71
|
rexbii |
⊢ ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = 𝑤 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
73 |
70 72
|
sylib |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
74 |
|
simpr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) → 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
75 |
74
|
inteqd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) → ∩ 𝑤 = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
76 |
75
|
eqeq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑤 = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) → ( ∅ = ∩ 𝑤 ↔ ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
77 |
53 73 76
|
rexxfrd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ∅ = ∩ 𝑤 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
78 |
|
0ex |
⊢ ∅ ∈ V |
79 |
|
imassrn |
⊢ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ⊆ ran ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) |
80 |
|
eqid |
⊢ ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) = ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) |
81 |
54 80
|
opncldf1 |
⊢ ( 𝐽 ∈ Top → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –1-1-onto→ ( Clsd ‘ 𝐽 ) ∧ ◡ ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) = ( 𝑣 ∈ ( Clsd ‘ 𝐽 ) ↦ ( ∪ 𝐽 ∖ 𝑣 ) ) ) ) |
82 |
81
|
simpld |
⊢ ( 𝐽 ∈ Top → ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –1-1-onto→ ( Clsd ‘ 𝐽 ) ) |
83 |
|
f1ofo |
⊢ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –1-1-onto→ ( Clsd ‘ 𝐽 ) → ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –onto→ ( Clsd ‘ 𝐽 ) ) |
84 |
82 83
|
syl |
⊢ ( 𝐽 ∈ Top → ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –onto→ ( Clsd ‘ 𝐽 ) ) |
85 |
|
forn |
⊢ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –onto→ ( Clsd ‘ 𝐽 ) → ran ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) = ( Clsd ‘ 𝐽 ) ) |
86 |
84 85
|
syl |
⊢ ( 𝐽 ∈ Top → ran ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) = ( Clsd ‘ 𝐽 ) ) |
87 |
79 86
|
sseqtrid |
⊢ ( 𝐽 ∈ Top → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ⊆ ( Clsd ‘ 𝐽 ) ) |
88 |
|
fvex |
⊢ ( Clsd ‘ 𝐽 ) ∈ V |
89 |
88
|
elpw2 |
⊢ ( ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∈ 𝒫 ( Clsd ‘ 𝐽 ) ↔ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ⊆ ( Clsd ‘ 𝐽 ) ) |
90 |
87 89
|
sylibr |
⊢ ( 𝐽 ∈ Top → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) |
91 |
90
|
ad2antrr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) |
92 |
|
elfi |
⊢ ( ( ∅ ∈ V ∧ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → ( ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ∅ = ∩ 𝑤 ) ) |
93 |
78 91 92
|
sylancr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( 𝒫 ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∩ Fin ) ∅ = ∩ 𝑤 ) ) |
94 |
|
inundif |
⊢ ( ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) = ( 𝒫 𝑦 ∩ Fin ) |
95 |
94
|
rexeqi |
⊢ ( ∃ 𝑧 ∈ ( ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) ∪ 𝐽 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) |
96 |
|
rexun |
⊢ ( ∃ 𝑧 ∈ ( ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) ∪ 𝐽 = ∪ 𝑧 ↔ ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ∨ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
97 |
95 96
|
bitr3i |
⊢ ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ↔ ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ∨ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
98 |
|
elinel2 |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) → 𝑧 ∈ { ∅ } ) |
99 |
|
elsni |
⊢ ( 𝑧 ∈ { ∅ } → 𝑧 = ∅ ) |
100 |
98 99
|
syl |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) → 𝑧 = ∅ ) |
101 |
100
|
unieqd |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) → ∪ 𝑧 = ∪ ∅ ) |
102 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
103 |
101 102
|
eqtrdi |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) → ∪ 𝑧 = ∅ ) |
104 |
103
|
eqeq2d |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) → ( ∪ 𝐽 = ∪ 𝑧 ↔ ∪ 𝐽 = ∅ ) ) |
105 |
104
|
biimpd |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) → ( ∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅ ) ) |
106 |
105
|
rexlimiv |
⊢ ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 → ∪ 𝐽 = ∅ ) |
107 |
|
ssidd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → 𝑦 ⊆ 𝑦 ) |
108 |
|
simprr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∪ 𝐽 = ∅ ) |
109 |
|
0ss |
⊢ ∅ ⊆ ∪ 𝑦 |
110 |
108 109
|
eqsstrdi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∪ 𝐽 ⊆ ∪ 𝑦 ) |
111 |
24
|
ad2antlr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∪ 𝑦 ⊆ ∪ 𝐽 ) |
112 |
110 111
|
eqssd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∪ 𝐽 = ∪ 𝑦 ) |
113 |
112 108
|
eqtr3d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∪ 𝑦 = ∅ ) |
114 |
113 3
|
eqeltrdi |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∪ 𝑦 ∈ Fin ) |
115 |
|
pwfi |
⊢ ( ∪ 𝑦 ∈ Fin ↔ 𝒫 ∪ 𝑦 ∈ Fin ) |
116 |
114 115
|
sylib |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → 𝒫 ∪ 𝑦 ∈ Fin ) |
117 |
|
pwuni |
⊢ 𝑦 ⊆ 𝒫 ∪ 𝑦 |
118 |
|
ssfi |
⊢ ( ( 𝒫 ∪ 𝑦 ∈ Fin ∧ 𝑦 ⊆ 𝒫 ∪ 𝑦 ) → 𝑦 ∈ Fin ) |
119 |
116 117 118
|
sylancl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → 𝑦 ∈ Fin ) |
120 |
|
elfpw |
⊢ ( 𝑦 ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝑦 ∧ 𝑦 ∈ Fin ) ) |
121 |
107 119 120
|
sylanbrc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → 𝑦 ∈ ( 𝒫 𝑦 ∩ Fin ) ) |
122 |
|
simprl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → 𝑦 ≠ ∅ ) |
123 |
|
eldifsn |
⊢ ( 𝑦 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑦 ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ 𝑦 ≠ ∅ ) ) |
124 |
121 122 123
|
sylanbrc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → 𝑦 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) |
125 |
|
unieq |
⊢ ( 𝑧 = 𝑦 → ∪ 𝑧 = ∪ 𝑦 ) |
126 |
125
|
rspceeqv |
⊢ ( ( 𝑦 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∧ ∪ 𝐽 = ∪ 𝑦 ) → ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) |
127 |
124 112 126
|
syl2anc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ ( 𝑦 ≠ ∅ ∧ ∪ 𝐽 = ∅ ) ) → ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) |
128 |
127
|
expr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∪ 𝐽 = ∅ → ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
129 |
106 128
|
syl5 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 → ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
130 |
|
idd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 → ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
131 |
129 130
|
jaod |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ∨ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) → ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
132 |
|
olc |
⊢ ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 → ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ∨ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
133 |
131 132
|
impbid1 |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∩ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ∨ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
134 |
97 133
|
syl5bb |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ) ) |
135 |
|
eldifi |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) → 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) |
136 |
135
|
adantl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ) |
137 |
|
elfpw |
⊢ ( 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ ( 𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin ) ) |
138 |
136 137
|
sylib |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( 𝑧 ⊆ 𝑦 ∧ 𝑧 ∈ Fin ) ) |
139 |
138
|
simpld |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → 𝑧 ⊆ 𝑦 ) |
140 |
|
simpllr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → 𝑦 ⊆ 𝐽 ) |
141 |
139 140
|
sstrd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → 𝑧 ⊆ 𝐽 ) |
142 |
141
|
unissd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∪ 𝑧 ⊆ ∪ 𝐽 ) |
143 |
|
eqss |
⊢ ( ∪ 𝑧 = ∪ 𝐽 ↔ ( ∪ 𝑧 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ ∪ 𝑧 ) ) |
144 |
143
|
baib |
⊢ ( ∪ 𝑧 ⊆ ∪ 𝐽 → ( ∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧 ) ) |
145 |
142 144
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( ∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 ⊆ ∪ 𝑧 ) ) |
146 |
|
eqcom |
⊢ ( ∪ 𝑧 = ∪ 𝐽 ↔ ∪ 𝐽 = ∪ 𝑧 ) |
147 |
|
ssdif0 |
⊢ ( ∪ 𝐽 ⊆ ∪ 𝑧 ↔ ( ∪ 𝐽 ∖ ∪ 𝑧 ) = ∅ ) |
148 |
|
eqcom |
⊢ ( ( ∪ 𝐽 ∖ ∪ 𝑧 ) = ∅ ↔ ∅ = ( ∪ 𝐽 ∖ ∪ 𝑧 ) ) |
149 |
147 148
|
bitri |
⊢ ( ∪ 𝐽 ⊆ ∪ 𝑧 ↔ ∅ = ( ∪ 𝐽 ∖ ∪ 𝑧 ) ) |
150 |
145 146 149
|
3bitr3g |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( ∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ( ∪ 𝐽 ∖ ∪ 𝑧 ) ) ) |
151 |
|
df-ima |
⊢ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ran ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑧 ) |
152 |
139
|
resmptd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑧 ) = ( 𝑟 ∈ 𝑧 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
153 |
152
|
rneqd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ran ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ↾ 𝑧 ) = ran ( 𝑟 ∈ 𝑧 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
154 |
151 153
|
syl5eq |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ran ( 𝑟 ∈ 𝑧 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
155 |
154
|
inteqd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ∩ ran ( 𝑟 ∈ 𝑧 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
156 |
56
|
ralrimivw |
⊢ ( 𝐽 ∈ Top → ∀ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V ) |
157 |
156
|
ad3antrrr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∀ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V ) |
158 |
|
dfiin3g |
⊢ ( ∀ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V → ∩ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ ran ( 𝑟 ∈ 𝑧 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
159 |
157 158
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ ran ( 𝑟 ∈ 𝑧 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
160 |
|
eldifsni |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) → 𝑧 ≠ ∅ ) |
161 |
160
|
adantl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → 𝑧 ≠ ∅ ) |
162 |
|
iindif2 |
⊢ ( 𝑧 ≠ ∅ → ∩ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟 ) ) |
163 |
161 162
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∩ 𝑟 ∈ 𝑧 ( ∪ 𝐽 ∖ 𝑟 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟 ) ) |
164 |
155 159 163
|
3eqtr2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟 ) ) |
165 |
|
uniiun |
⊢ ∪ 𝑧 = ∪ 𝑟 ∈ 𝑧 𝑟 |
166 |
165
|
difeq2i |
⊢ ( ∪ 𝐽 ∖ ∪ 𝑧 ) = ( ∪ 𝐽 ∖ ∪ 𝑟 ∈ 𝑧 𝑟 ) |
167 |
164 166
|
eqtr4di |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ( ∪ 𝐽 ∖ ∪ 𝑧 ) ) |
168 |
167
|
eqeq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ↔ ∅ = ( ∪ 𝐽 ∖ ∪ 𝑧 ) ) ) |
169 |
150 168
|
bitr4d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) ∧ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) → ( ∪ 𝐽 = ∪ 𝑧 ↔ ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
170 |
169
|
rexbidva |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∪ 𝐽 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
171 |
134 170
|
bitrd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
172 |
|
imaeq2 |
⊢ ( 𝑧 = ∅ → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ ∅ ) ) |
173 |
|
ima0 |
⊢ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ ∅ ) = ∅ |
174 |
172 173
|
eqtrdi |
⊢ ( 𝑧 = ∅ → ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ∅ ) |
175 |
174
|
inteqd |
⊢ ( 𝑧 = ∅ → ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = ∩ ∅ ) |
176 |
|
int0 |
⊢ ∩ ∅ = V |
177 |
175 176
|
eqtrdi |
⊢ ( 𝑧 = ∅ → ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) = V ) |
178 |
177
|
neeq1d |
⊢ ( 𝑧 = ∅ → ( ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ≠ ∅ ↔ V ≠ ∅ ) ) |
179 |
14 178
|
mpbiri |
⊢ ( 𝑧 = ∅ → ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ≠ ∅ ) |
180 |
179
|
necomd |
⊢ ( 𝑧 = ∅ → ∅ ≠ ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
181 |
180
|
necon2i |
⊢ ( ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) → 𝑧 ≠ ∅ ) |
182 |
|
eldifsn |
⊢ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ↔ ( 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ 𝑧 ≠ ∅ ) ) |
183 |
182
|
rbaibr |
⊢ ( 𝑧 ≠ ∅ → ( 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) ) |
184 |
181 183
|
syl |
⊢ ( ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) → ( 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ↔ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ) ) |
185 |
184
|
pm5.32ri |
⊢ ( ( 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∧ ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ↔ ( 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∧ ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
186 |
185
|
rexbii2 |
⊢ ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ↔ ∃ 𝑧 ∈ ( ( 𝒫 𝑦 ∩ Fin ) ∖ { ∅ } ) ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) |
187 |
171 186
|
bitr4di |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∅ = ∩ ( ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑧 ) ) ) |
188 |
77 93 187
|
3bitr4rd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ↔ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) |
189 |
38 188
|
imbi12d |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) ∧ 𝑦 ≠ ∅ ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) ) |
190 |
23 189
|
pm2.61dane |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) ) |
191 |
57
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ∀ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V ) |
192 |
|
dfiin3g |
⊢ ( ∀ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) ∈ V → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
193 |
191 192
|
syl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
194 |
44
|
inteqd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ∩ ran ( 𝑟 ∈ 𝑦 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
195 |
193 194
|
eqtr4d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) |
196 |
195
|
eqeq1d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ↔ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ∅ ) ) |
197 |
|
nne |
⊢ ( ¬ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ↔ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) = ∅ ) |
198 |
196 197
|
bitr4di |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ ↔ ¬ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) |
199 |
198
|
imbi1d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ( ∩ 𝑟 ∈ 𝑦 ( ∪ 𝐽 ∖ 𝑟 ) = ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ↔ ( ¬ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) ) |
200 |
190 199
|
bitrd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ( ¬ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) ) |
201 |
|
con1b |
⊢ ( ( ¬ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ → ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ↔ ( ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) |
202 |
200 201
|
bitrdi |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ⊆ 𝐽 ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ( ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) ) |
203 |
1 202
|
sylan2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽 ) → ( ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ( ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) ) |
204 |
203
|
ralbidva |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) ) |
205 |
54
|
iscmp |
⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) ) |
206 |
205
|
baib |
⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( ∪ 𝐽 = ∪ 𝑦 → ∃ 𝑧 ∈ ( 𝒫 𝑦 ∩ Fin ) ∪ 𝐽 = ∪ 𝑧 ) ) ) |
207 |
90
|
adantr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝒫 𝐽 ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) |
208 |
|
simpl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top ) |
209 |
|
funmpt |
⊢ Fun ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) |
210 |
209
|
a1i |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → Fun ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ) |
211 |
|
elpwi |
⊢ ( 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ ( Clsd ‘ 𝐽 ) ) |
212 |
|
foima |
⊢ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) : 𝐽 –onto→ ( Clsd ‘ 𝐽 ) → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝐽 ) = ( Clsd ‘ 𝐽 ) ) |
213 |
84 212
|
syl |
⊢ ( 𝐽 ∈ Top → ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝐽 ) = ( Clsd ‘ 𝐽 ) ) |
214 |
213
|
sseq2d |
⊢ ( 𝐽 ∈ Top → ( 𝑥 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝐽 ) ↔ 𝑥 ⊆ ( Clsd ‘ 𝐽 ) ) ) |
215 |
211 214
|
syl5ibr |
⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝐽 ) ) ) |
216 |
215
|
imp |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → 𝑥 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝐽 ) ) |
217 |
|
ssimaexg |
⊢ ( ( 𝐽 ∈ Top ∧ Fun ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) ∧ 𝑥 ⊆ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝐽 ) ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
218 |
208 210 216 217
|
syl3anc |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
219 |
|
df-rex |
⊢ ( ∃ 𝑦 ∈ 𝒫 𝐽 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
220 |
|
velpw |
⊢ ( 𝑦 ∈ 𝒫 𝐽 ↔ 𝑦 ⊆ 𝐽 ) |
221 |
220
|
anbi1i |
⊢ ( ( 𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ↔ ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
222 |
221
|
exbii |
⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝒫 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
223 |
219 222
|
bitri |
⊢ ( ∃ 𝑦 ∈ 𝒫 𝐽 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ⊆ 𝐽 ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
224 |
218 223
|
sylibr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) → ∃ 𝑦 ∈ 𝒫 𝐽 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) |
225 |
|
simpr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) |
226 |
225
|
fveq2d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ( fi ‘ 𝑥 ) = ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) |
227 |
226
|
eleq2d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ( ∅ ∈ ( fi ‘ 𝑥 ) ↔ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) |
228 |
227
|
notbid |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) ) ) |
229 |
225
|
inteqd |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ 𝑥 = ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) |
230 |
229
|
neeq1d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ( ∩ 𝑥 ≠ ∅ ↔ ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) |
231 |
228 230
|
imbi12d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ( ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ↔ ( ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) ) |
232 |
207 224 231
|
ralxfrd |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ↔ ∀ 𝑦 ∈ 𝒫 𝐽 ( ¬ ∅ ∈ ( fi ‘ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ) → ∩ ( ( 𝑟 ∈ 𝐽 ↦ ( ∪ 𝐽 ∖ 𝑟 ) ) “ 𝑦 ) ≠ ∅ ) ) ) |
233 |
204 206 232
|
3bitr4d |
⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) ) |