Metamath Proof Explorer


Theorem cnss2

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

Ref Expression
Hypothesis cnss2.1 𝑌 = 𝐾
Assertion cnss2 ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) → ( 𝐽 Cn 𝐾 ) ⊆ ( 𝐽 Cn 𝐿 ) )

Proof

Step Hyp Ref Expression
1 cnss2.1 𝑌 = 𝐾
2 eqid 𝐽 = 𝐽
3 2 1 cnf ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 : 𝐽𝑌 )
4 3 adantl ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 : 𝐽𝑌 )
5 simplr ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐿𝐾 )
6 cnima ( ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑥𝐾 ) → ( 𝑓𝑥 ) ∈ 𝐽 )
7 6 ralrimiva ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → ∀ 𝑥𝐾 ( 𝑓𝑥 ) ∈ 𝐽 )
8 7 adantl ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥𝐾 ( 𝑓𝑥 ) ∈ 𝐽 )
9 ssralv ( 𝐿𝐾 → ( ∀ 𝑥𝐾 ( 𝑓𝑥 ) ∈ 𝐽 → ∀ 𝑥𝐿 ( 𝑓𝑥 ) ∈ 𝐽 ) )
10 5 8 9 sylc ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥𝐿 ( 𝑓𝑥 ) ∈ 𝐽 )
11 cntop1 ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
12 11 adantl ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top )
13 toptopon2 ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
14 12 13 sylib ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ ( TopOn ‘ 𝐽 ) )
15 simpll ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
16 iscn ( ( 𝐽 ∈ ( TopOn ‘ 𝐽 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ↔ ( 𝑓 : 𝐽𝑌 ∧ ∀ 𝑥𝐿 ( 𝑓𝑥 ) ∈ 𝐽 ) ) )
17 14 15 16 syl2anc ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ↔ ( 𝑓 : 𝐽𝑌 ∧ ∀ 𝑥𝐿 ( 𝑓𝑥 ) ∈ 𝐽 ) ) )
18 4 10 17 mpbir2and ( ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) ∧ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑓 ∈ ( 𝐽 Cn 𝐿 ) )
19 18 ex ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝑓 ∈ ( 𝐽 Cn 𝐿 ) ) )
20 19 ssrdv ( ( 𝐿 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿𝐾 ) → ( 𝐽 Cn 𝐾 ) ⊆ ( 𝐽 Cn 𝐿 ) )