# Metamath Proof Explorer

## Theorem iscn

Description: The predicate "the class F is a continuous function from topology J to topology K ". Definition of continuous function in Munkres p. 102. (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscn ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)\right)$

### Proof

Step Hyp Ref Expression
1 cnfval ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to {J}\mathrm{Cn}{K}=\left\{{f}\in \left({{Y}}^{{X}}\right)|\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{y}\right]\in {J}\right\}$
2 1 eleq2d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)↔{F}\in \left\{{f}\in \left({{Y}}^{{X}}\right)|\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{y}\right]\in {J}\right\}\right)$
3 cnveq ${⊢}{f}={F}\to {{f}}^{-1}={{F}}^{-1}$
4 3 imaeq1d ${⊢}{f}={F}\to {{f}}^{-1}\left[{y}\right]={{F}}^{-1}\left[{y}\right]$
5 4 eleq1d ${⊢}{f}={F}\to \left({{f}}^{-1}\left[{y}\right]\in {J}↔{{F}}^{-1}\left[{y}\right]\in {J}\right)$
6 5 ralbidv ${⊢}{f}={F}\to \left(\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{y}\right]\in {J}↔\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)$
7 6 elrab ${⊢}{F}\in \left\{{f}\in \left({{Y}}^{{X}}\right)|\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{y}\right]\in {J}\right\}↔\left({F}\in \left({{Y}}^{{X}}\right)\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)$
8 toponmax ${⊢}{K}\in \mathrm{TopOn}\left({Y}\right)\to {Y}\in {K}$
9 toponmax ${⊢}{J}\in \mathrm{TopOn}\left({X}\right)\to {X}\in {J}$
10 elmapg ${⊢}\left({Y}\in {K}\wedge {X}\in {J}\right)\to \left({F}\in \left({{Y}}^{{X}}\right)↔{F}:{X}⟶{Y}\right)$
11 8 9 10 syl2anr ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({{Y}}^{{X}}\right)↔{F}:{X}⟶{Y}\right)$
12 11 anbi1d ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left(\left({F}\in \left({{Y}}^{{X}}\right)\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)\right)$
13 7 12 syl5bb ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left\{{f}\in \left({{Y}}^{{X}}\right)|\forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{f}}^{-1}\left[{y}\right]\in {J}\right\}↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)\right)$
14 2 13 bitrd ${⊢}\left({J}\in \mathrm{TopOn}\left({X}\right)\wedge {K}\in \mathrm{TopOn}\left({Y}\right)\right)\to \left({F}\in \left({J}\mathrm{Cn}{K}\right)↔\left({F}:{X}⟶{Y}\wedge \forall {y}\in {K}\phantom{\rule{.4em}{0ex}}{{F}}^{-1}\left[{y}\right]\in {J}\right)\right)$