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 = ⋃ J$
	Assertion	cnss1	$⊢ (K \in TopOn (X) \land J \subseteq K) \to J Cn L \subseteq K Cn L$

Proof

Step	Hyp	Ref	Expression
1		cnss1.1	$⊢ X = ⋃ J$
2		eqid	$⊢ ⋃ L = ⋃ L$
3	1 2	cnf	$⊢ f \in (J Cn L) \to f : X ⟶ ⋃ L$
4	3	adantl	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to f : X ⟶ ⋃ L$
5		simpllr	$⊢ (((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \land x \in L) \to J \subseteq K$
6		cnima	$⊢ (f \in (J Cn L) \land x \in L) \to f^{-1} [x] \in J$
7	6	adantll	$⊢ (((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \land x \in L) \to f^{-1} [x] \in J$
8	5 7	sseldd	$⊢ (((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \land x \in L) \to f^{-1} [x] \in K$
9	8	ralrimiva	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to \forall x \in L f^{-1} [x] \in K$
10		simpll	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to K \in TopOn (X)$
11		cntop2	$⊢ f \in (J Cn L) \to L \in Top$
12	11	adantl	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to L \in Top$
13		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
14	12 13	sylib	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to L \in TopOn (⋃ L)$
15		iscn	$⊢ (K \in TopOn (X) \land L \in TopOn (⋃ L)) \to (f \in (K Cn L) \leftrightarrow (f : X ⟶ ⋃ L \land \forall x \in L f^{-1} [x] \in K))$
16	10 14 15	syl2anc	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to (f \in (K Cn L) \leftrightarrow (f : X ⟶ ⋃ L \land \forall x \in L f^{-1} [x] \in K))$
17	4 9 16	mpbir2and	$⊢ ((K \in TopOn (X) \land J \subseteq K) \land f \in (J Cn L)) \to f \in (K Cn L)$
18	17	ex	$⊢ (K \in TopOn (X) \land J \subseteq K) \to (f \in (J Cn L) \to f \in (K Cn L))$
19	18	ssrdv	$⊢ (K \in TopOn (X) \land J \subseteq K) \to J Cn L \subseteq K Cn L$