This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cncls2i

Description: Property of the preimage of a closure. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis cncls2i.1 ⊢ 𝑌 = ∪ 𝐾
Assertion cncls2i ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑆 ⊆ 𝑌 ) → ( ( cls ‘ 𝐽 ) ‘ ( ◡ 𝐹 “ 𝑆 ) ) ⊆ ( ◡ 𝐹 “ ( ( cls ‘ 𝐾 ) ‘ 𝑆 ) ) )

Proof

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 ‘ 𝐾 ) ‘ 𝑆 ) ) )