Step |
Hyp |
Ref |
Expression |
1 |
|
ist0.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
iunid |
⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴 |
3 |
1
|
ist1 |
⊢ ( 𝐽 ∈ Fre ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) ) |
4 |
3
|
simplbi |
⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top ) |
5 |
4
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin ) → 𝐽 ∈ Top ) |
6 |
|
simp3 |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin ) |
7 |
3
|
simprbi |
⊢ ( 𝐽 ∈ Fre → ∀ 𝑥 ∈ 𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) |
8 |
|
ssralv |
⊢ ( 𝐴 ⊆ 𝑋 → ( ∀ 𝑥 ∈ 𝑋 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) → ∀ 𝑥 ∈ 𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) ) |
9 |
7 8
|
mpan9 |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ) → ∀ 𝑥 ∈ 𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin ) → ∀ 𝑥 ∈ 𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) |
11 |
1
|
iuncld |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) → ∪ 𝑥 ∈ 𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) |
12 |
5 6 10 11
|
syl3anc |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin ) → ∪ 𝑥 ∈ 𝐴 { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ) |
13 |
2 12
|
eqeltrrid |
⊢ ( ( 𝐽 ∈ Fre ∧ 𝐴 ⊆ 𝑋 ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) ) |