Theorem cvmfo

Description: A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Hypotheses	cvmlift.1	$$⊢B=\bigcup C$$
	cvmfo.2	$$⊢X=\bigcup J$$
Assertion	cvmfo	$$⊢F\in \left(C\mathrm{CovMap}J\right)\to F:B\underset{onto}{⟶}X$$

Proof

Step	Hyp	Ref	Expression
1		cvmlift.1	$$⊢B=\bigcup C$$
2		cvmfo.2	$$⊢X=\bigcup J$$
3		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)$$
4	3	cvmscbv	$$⊢\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(a\in J⟼\left\{b\in \left(𝒫C\setminus \left\{\varnothing \right\}\right)|\left(\bigcup b=F^{-1}\left[a\right]\wedge \forall c\in b\left(\forall d\in \left(b\setminus \left\{c\right\}\right)c\cap d=\varnothing \wedge {F\upharpoonright }_c\in \left(\left(C{\upharpoonright }_{𝑡}c\right)\mathrm{Homeo}\left(J{\upharpoonright }_{𝑡}a\right)\right)\right)\right)\right\}\right)$$
5	4 1 2	cvmfolem	$$⊢F\in \left(C\mathrm{CovMap}J\right)\to F:B\underset{onto}{⟶}X$$