Step |
Hyp |
Ref |
Expression |
1 |
|
fvex |
⊢ ( Clsd ‘ 𝐽 ) ∈ V |
2 |
1
|
elpw2 |
⊢ ( 𝑋 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ↔ 𝑋 ⊆ ( Clsd ‘ 𝐽 ) ) |
3 |
2
|
biimpri |
⊢ ( 𝑋 ⊆ ( Clsd ‘ 𝐽 ) → 𝑋 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ) |
4 |
|
cmptop |
⊢ ( 𝐽 ∈ Comp → 𝐽 ∈ Top ) |
5 |
|
cmpfi |
⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) ) |
6 |
4 5
|
syl |
⊢ ( 𝐽 ∈ Comp → ( 𝐽 ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) ) |
7 |
6
|
ibi |
⊢ ( 𝐽 ∈ Comp → ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) |
8 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( fi ‘ 𝑥 ) = ( fi ‘ 𝑋 ) ) |
9 |
8
|
eleq2d |
⊢ ( 𝑥 = 𝑋 → ( ∅ ∈ ( fi ‘ 𝑥 ) ↔ ∅ ∈ ( fi ‘ 𝑋 ) ) ) |
10 |
9
|
notbid |
⊢ ( 𝑥 = 𝑋 → ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( fi ‘ 𝑋 ) ) ) |
11 |
|
inteq |
⊢ ( 𝑥 = 𝑋 → ∩ 𝑥 = ∩ 𝑋 ) |
12 |
11
|
neeq1d |
⊢ ( 𝑥 = 𝑋 → ( ∩ 𝑥 ≠ ∅ ↔ ∩ 𝑋 ≠ ∅ ) ) |
13 |
10 12
|
imbi12d |
⊢ ( 𝑥 = 𝑋 → ( ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ↔ ( ¬ ∅ ∈ ( fi ‘ 𝑋 ) → ∩ 𝑋 ≠ ∅ ) ) ) |
14 |
13
|
rspcva |
⊢ ( ( 𝑋 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ∧ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → ∩ 𝑥 ≠ ∅ ) ) → ( ¬ ∅ ∈ ( fi ‘ 𝑋 ) → ∩ 𝑋 ≠ ∅ ) ) |
15 |
3 7 14
|
syl2anr |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝑋 ⊆ ( Clsd ‘ 𝐽 ) ) → ( ¬ ∅ ∈ ( fi ‘ 𝑋 ) → ∩ 𝑋 ≠ ∅ ) ) |
16 |
15
|
3impia |
⊢ ( ( 𝐽 ∈ Comp ∧ 𝑋 ⊆ ( Clsd ‘ 𝐽 ) ∧ ¬ ∅ ∈ ( fi ‘ 𝑋 ) ) → ∩ 𝑋 ≠ ∅ ) |