# 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}=\bigcup {J}$
Assertion cnss1 ${⊢}\left({K}\in \mathrm{TopOn}\left({X}\right)\wedge {J}\subseteq {K}\right)\to {J}\mathrm{Cn}{L}\subseteq {K}\mathrm{Cn}{L}$

### Proof

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