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

Proof

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