Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
2 |
1
|
fclsfil |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) |
3 |
|
fclstopon |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) ) |
4 |
2 3
|
mpbird |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ) |
5 |
|
fclsopn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ ∪ 𝐽 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) ) |
6 |
4 2 5
|
syl2anc |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ↔ ( 𝐴 ∈ ∪ 𝐽 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) ) |
7 |
6
|
ibi |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝐴 ∈ ∪ 𝐽 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ) ) |
8 |
|
eleq2 |
⊢ ( 𝑜 = 𝑈 → ( 𝐴 ∈ 𝑜 ↔ 𝐴 ∈ 𝑈 ) ) |
9 |
|
ineq1 |
⊢ ( 𝑜 = 𝑈 → ( 𝑜 ∩ 𝑠 ) = ( 𝑈 ∩ 𝑠 ) ) |
10 |
9
|
neeq1d |
⊢ ( 𝑜 = 𝑈 → ( ( 𝑜 ∩ 𝑠 ) ≠ ∅ ↔ ( 𝑈 ∩ 𝑠 ) ≠ ∅ ) ) |
11 |
10
|
ralbidv |
⊢ ( 𝑜 = 𝑈 → ( ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ↔ ∀ 𝑠 ∈ 𝐹 ( 𝑈 ∩ 𝑠 ) ≠ ∅ ) ) |
12 |
8 11
|
imbi12d |
⊢ ( 𝑜 = 𝑈 → ( ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) ↔ ( 𝐴 ∈ 𝑈 → ∀ 𝑠 ∈ 𝐹 ( 𝑈 ∩ 𝑠 ) ≠ ∅ ) ) ) |
13 |
12
|
rspccv |
⊢ ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∀ 𝑠 ∈ 𝐹 ( 𝑜 ∩ 𝑠 ) ≠ ∅ ) → ( 𝑈 ∈ 𝐽 → ( 𝐴 ∈ 𝑈 → ∀ 𝑠 ∈ 𝐹 ( 𝑈 ∩ 𝑠 ) ≠ ∅ ) ) ) |
14 |
7 13
|
simpl2im |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝑈 ∈ 𝐽 → ( 𝐴 ∈ 𝑈 → ∀ 𝑠 ∈ 𝐹 ( 𝑈 ∩ 𝑠 ) ≠ ∅ ) ) ) |
15 |
|
ineq2 |
⊢ ( 𝑠 = 𝑆 → ( 𝑈 ∩ 𝑠 ) = ( 𝑈 ∩ 𝑆 ) ) |
16 |
15
|
neeq1d |
⊢ ( 𝑠 = 𝑆 → ( ( 𝑈 ∩ 𝑠 ) ≠ ∅ ↔ ( 𝑈 ∩ 𝑆 ) ≠ ∅ ) ) |
17 |
16
|
rspccv |
⊢ ( ∀ 𝑠 ∈ 𝐹 ( 𝑈 ∩ 𝑠 ) ≠ ∅ → ( 𝑆 ∈ 𝐹 → ( 𝑈 ∩ 𝑆 ) ≠ ∅ ) ) |
18 |
14 17
|
syl8 |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → ( 𝑈 ∈ 𝐽 → ( 𝐴 ∈ 𝑈 → ( 𝑆 ∈ 𝐹 → ( 𝑈 ∩ 𝑆 ) ≠ ∅ ) ) ) ) |
19 |
18
|
3imp2 |
⊢ ( ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ∧ 𝑆 ∈ 𝐹 ) ) → ( 𝑈 ∩ 𝑆 ) ≠ ∅ ) |