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

Proof

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