Metamath Proof Explorer

Theorem elqtop

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

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

Proof

Step	Hyp	Ref	Expression
1		qtopval.1	$⊢ X = ⋃ J$
2	1	qtopval2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to J qTop F = \{s \in 𝒫 Y \| F^{-1} [s] \in J\}$
3	2	eleq2d	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to (A \in (J qTop F) \leftrightarrow A \in \{s \in 𝒫 Y \| F^{-1} [s] \in J\})$
4		imaeq2	$⊢ s = A \to F^{-1} [s] = F^{-1} [A]$
5	4	eleq1d	$⊢ s = A \to (F^{-1} [s] \in J \leftrightarrow F^{-1} [A] \in J)$
6	5	elrab	$⊢ A \in \{s \in 𝒫 Y \| F^{-1} [s] \in J\} \leftrightarrow (A \in 𝒫 Y \land F^{-1} [A] \in J)$
7		uniexg	$⊢ J \in V \to ⋃ J \in V$
8	1 7	eqeltrid	$⊢ J \in V \to X \in V$
9	8	3ad2ant1	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to X \in V$
10		simp3	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Z \subseteq X$
11	9 10	ssexd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Z \in V$
12		simp2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F : Z \underset{onto}{⟶} Y$
13		fornex	$⊢ Z \in V \to (F : Z \underset{onto}{⟶} Y \to Y \in V)$
14	11 12 13	sylc	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Y \in V$
15		elpw2g	$⊢ Y \in V \to (A \in 𝒫 Y \leftrightarrow A \subseteq Y)$
16	14 15	syl	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to (A \in 𝒫 Y \leftrightarrow A \subseteq Y)$
17	16	anbi1d	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to ((A \in 𝒫 Y \land F^{-1} [A] \in J) \leftrightarrow (A \subseteq Y \land F^{-1} [A] \in J))$
18	6 17	syl5bb	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to (A \in \{s \in 𝒫 Y \| F^{-1} [s] \in J\} \leftrightarrow (A \subseteq Y \land F^{-1} [A] \in J))$
19	3 18	bitrd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to (A \in (J qTop F) \leftrightarrow (A \subseteq Y \land F^{-1} [A] \in J))$