Step |
Hyp |
Ref |
Expression |
1 |
|
fclselbas.1 |
⊢ 𝑋 = ∪ 𝐽 |
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 |
7
|
simpld |
⊢ ( 𝐴 ∈ ( 𝐽 fClus 𝐹 ) → 𝐴 ∈ 𝑋 ) |