Step |
Hyp |
Ref |
Expression |
1 |
|
cncls2i.1 |
⊢ 𝑌 = ∪ 𝐾 |
2 |
|
cntop2 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top ) |
3 |
1
|
clscld |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ 𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐾 ) ) |
4 |
2 3
|
sylan |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐾 ) ) |
5 |
|
cnclima |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐾 ) ) → ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ 𝐽 ) ) |
6 |
4 5
|
syldan |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ 𝐽 ) ) |
7 |
1
|
sscls |
⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) |
8 |
2 7
|
sylan |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) |
9 |
|
imass2 |
⊢ ( 𝑆 ⊆ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) → ( ◡ 𝐹 “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) |
10 |
8 9
|
syl |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ◡ 𝐹 “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) |
11 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
12 |
11
|
clsss2 |
⊢ ( ( ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ◡ 𝐹 “ 𝑆 ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑆 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) |
13 |
6 10 12
|
syl2anc |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑆 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) ) |