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