Theorem cvmopn

Description: A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015)

	Ref	Expression
Assertion	cvmopn	$$⊢\left(F\in \left(C\mathrm{CovMap}J\right)\wedge A\in C\right)\to F\left[A\right]\in J$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(k\in J⟼\left\{s\in \left(𝒫C\setminus \left\{\varnothing \right\}\right)|\left(\bigcup s=F^{-1}\left[k\right]\wedge \forall u\in s\left(\forall v\in \left(s\setminus \left\{u\right\}\right)u\cap v=\varnothing \wedge {F\upharpoonright }_u\in \left(\left(C{\upharpoonright }_{𝑡}u\right)\mathrm{Homeo}\left(J{\upharpoonright }_{𝑡}k\right)\right)\right)\right)\right\}\right)=\left(k\in J⟼\left\{s\in \left(𝒫C\setminus \left\{\varnothing \right\}\right)|\left(\bigcup s=F^{-1}\left[k\right]\wedge \forall u\in s\left(\forall v\in \left(s\setminus \left\{u\right\}\right)u\cap v=\varnothing \wedge {F\upharpoonright }_u\in \left(\left(C{\upharpoonright }_{𝑡}u\right)\mathrm{Homeo}\left(J{\upharpoonright }_{𝑡}k\right)\right)\right)\right)\right\}\right)$$
2		eqid	$$⊢\bigcup C=\bigcup C$$
3	1 2	cvmopnlem	$$⊢\left(F\in \left(C\mathrm{CovMap}J\right)\wedge A\in C\right)\to F\left[A\right]\in J$$