Theorem elqtop2

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Hypothesis	qtoptop.1	$$⊢X=\bigcup J$$
Assertion	elqtop2	$$⊢\left(J\in V\wedge F:X\underset{onto}{⟶}Y\right)\to \left(A\in \left(J\mathrm{qTop}F\right)\leftrightarrow \left(A\subseteq Y\wedge F^{-1}\left[A\right]\in J\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		qtoptop.1	$$⊢X=\bigcup J$$
2		ssid	$$⊢X\subseteq X$$
3	1	elqtop	$$⊢\left(J\in V\wedge F:X\underset{onto}{⟶}Y\wedge X\subseteq X\right)\to \left(A\in \left(J\mathrm{qTop}F\right)\leftrightarrow \left(A\subseteq Y\wedge F^{-1}\left[A\right]\in J\right)\right)$$
4	2 3	mp3an3	$$⊢\left(J\in V\wedge F:X\underset{onto}{⟶}Y\right)\to \left(A\in \left(J\mathrm{qTop}F\right)\leftrightarrow \left(A\subseteq Y\wedge F^{-1}\left[A\right]\in J\right)\right)$$