This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )