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