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

Metamath Proof Explorer

Theorem cnss1

Description: If the topology K is finer than J , then there are more continuous functions from K than from J . (Contributed by Mario Carneiro, 19-Mar-2015) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypothesis cnss1.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cnss1 ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐽 Cn 𝐿 ) ⊆ ( 𝐾 Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnss1.1 ⊢ 𝑋 = ∪ 𝐽
2 eqid ⊢ ∪ 𝐿 = ∪ 𝐿
3 1 2 cnf ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) → 𝑓 : 𝑋 ⟶ ∪ 𝐿 )
4 3 adantl ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → 𝑓 : 𝑋 ⟶ ∪ 𝐿 )
5 simpllr ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → 𝐽 ⊆ 𝐾 )
6 cnima ⊢ ( ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
7 6 adantll ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐽 )
8 5 7 sseldd ⊢ ( ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) ∧ 𝑥 ∈ 𝐿 ) → ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐾 )
9 8 ralrimiva ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐾 )
10 simpll ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
11 cntop2 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) → 𝐿 ∈ Top )
12 11 adantl ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → 𝐿 ∈ Top )
13 toptopon2 ⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
14 12 13 sylib ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
15 iscn ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ) → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) ↔ ( 𝑓 : 𝑋 ⟶ ∪ 𝐿 ∧ ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐾 ) ) )
16 10 14 15 syl2anc ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → ( 𝑓 ∈ ( 𝐾 Cn 𝐿 ) ↔ ( 𝑓 : 𝑋 ⟶ ∪ 𝐿 ∧ ∀ 𝑥 ∈ 𝐿 ( ◡ 𝑓 “ 𝑥 ) ∈ 𝐾 ) ) )
17 4 9 16 mpbir2and ⊢ ( ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) → 𝑓 ∈ ( 𝐾 Cn 𝐿 ) )
18 17 ex ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) → 𝑓 ∈ ( 𝐾 Cn 𝐿 ) ) )
19 18 ssrdv ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐽 Cn 𝐿 ) ⊆ ( 𝐾 Cn 𝐿 ) )