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 ⊢ Y = ⋃ K
Assertion cnss2 ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K → J Cn K ⊆ J Cn L

Proof

Step Hyp Ref Expression
1 cnss2.1 ⊢ Y = ⋃ K
2 eqid ⊢ ⋃ J = ⋃ J
3 2 1 cnf ⊢ f ∈ J Cn K → f : ⋃ J ⟶ Y
4 3 adantl ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → f : ⋃ J ⟶ Y
5 simplr ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → L ⊆ K
6 cnima ⊢ f ∈ J Cn K ∧ x ∈ K → f -1 x ∈ J
7 6 ralrimiva ⊢ f ∈ J Cn K → ∀ x ∈ K f -1 x ∈ J
8 7 adantl ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → ∀ x ∈ K f -1 x ∈ J
9 ssralv ⊢ L ⊆ K → ∀ x ∈ K f -1 x ∈ J → ∀ x ∈ L f -1 x ∈ J
10 5 8 9 sylc ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → ∀ x ∈ L f -1 x ∈ J
11 cntop1 ⊢ f ∈ J Cn K → J ∈ Top
12 11 adantl ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → J ∈ Top
13 toptopon2 ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ ⋃ J
14 12 13 sylib ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → J ∈ TopOn ⁡ ⋃ J
15 simpll ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → L ∈ TopOn ⁡ Y
16 iscn ⊢ J ∈ TopOn ⁡ ⋃ J ∧ L ∈ TopOn ⁡ Y → f ∈ J Cn L ↔ f : ⋃ J ⟶ Y ∧ ∀ x ∈ L f -1 x ∈ J
17 14 15 16 syl2anc ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → f ∈ J Cn L ↔ f : ⋃ J ⟶ Y ∧ ∀ x ∈ L f -1 x ∈ J
18 4 10 17 mpbir2and ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K ∧ f ∈ J Cn K → f ∈ J Cn L
19 18 ex ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K → f ∈ J Cn K → f ∈ J Cn L
20 19 ssrdv ⊢ L ∈ TopOn ⁡ Y ∧ L ⊆ K → J Cn K ⊆ J Cn L