This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elqtop2

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

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

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