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 = U. J
Assertion cnss1
|- ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( J Cn L ) C_ ( K Cn L ) )

Proof

Step Hyp Ref Expression
1 cnss1.1
 |-  X = U. J
2 eqid
 |-  U. L = U. L
3 1 2 cnf
 |-  ( f e. ( J Cn L ) -> f : X --> U. L )
4 3 adantl
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> f : X --> U. L )
5 simpllr
 |-  ( ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) /\ x e. L ) -> J C_ K )
6 cnima
 |-  ( ( f e. ( J Cn L ) /\ x e. L ) -> ( `' f " x ) e. J )
7 6 adantll
 |-  ( ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) /\ x e. L ) -> ( `' f " x ) e. J )
8 5 7 sseldd
 |-  ( ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) /\ x e. L ) -> ( `' f " x ) e. K )
9 8 ralrimiva
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> A. x e. L ( `' f " x ) e. K )
10 simpll
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> K e. ( TopOn ` X ) )
11 cntop2
 |-  ( f e. ( J Cn L ) -> L e. Top )
12 11 adantl
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> L e. Top )
13 toptopon2
 |-  ( L e. Top <-> L e. ( TopOn ` U. L ) )
14 12 13 sylib
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> L e. ( TopOn ` U. L ) )
15 iscn
 |-  ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` U. L ) ) -> ( f e. ( K Cn L ) <-> ( f : X --> U. L /\ A. x e. L ( `' f " x ) e. K ) ) )
16 10 14 15 syl2anc
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> ( f e. ( K Cn L ) <-> ( f : X --> U. L /\ A. x e. L ( `' f " x ) e. K ) ) )
17 4 9 16 mpbir2and
 |-  ( ( ( K e. ( TopOn ` X ) /\ J C_ K ) /\ f e. ( J Cn L ) ) -> f e. ( K Cn L ) )
18 17 ex
 |-  ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( f e. ( J Cn L ) -> f e. ( K Cn L ) ) )
19 18 ssrdv
 |-  ( ( K e. ( TopOn ` X ) /\ J C_ K ) -> ( J Cn L ) C_ ( K Cn L ) )