elqtop3

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

		Ref	Expression
	Assertion	elqtop3	$⊢ (J \in TopOn (X) \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		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
2		eqimss	$⊢ X = ⋃ J \to X \subseteq ⋃ J$
3	1 2	syl	$⊢ J \in TopOn (X) \to X \subseteq ⋃ J$
4	3	adantr	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to X \subseteq ⋃ J$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	5	elqtop	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y \land X \subseteq ⋃ J) \to (A \in (J qTop F) \leftrightarrow (A \subseteq Y \land F^{-1} [A] \in J))$
7	4 6	mpd3an3	$⊢ (J \in TopOn (X) \land F : X \underset{onto}{⟶} Y) \to (A \in (J qTop F) \leftrightarrow (A \subseteq Y \land F^{-1} [A] \in J))$

Metamath Proof Explorer