qtopval

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

		Ref	Expression
	Hypothesis	qtopval.1	$⊢ X = ⋃ J$
	Assertion	qtopval	$⊢ (J \in V \land F \in W) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$

Proof

Step	Hyp	Ref	Expression
1		qtopval.1	$⊢ X = ⋃ J$
2		elex	$⊢ J \in V \to J \in V$
3		elex	$⊢ F \in W \to F \in V$
4		imaexg	$⊢ F \in V \to F [X] \in V$
5		pwexg	$⊢ F [X] \in V \to 𝒫 F [X] \in V$
6		rabexg	$⊢ 𝒫 F [X] \in V \to \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\} \in V$
7	4 5 6	3syl	$⊢ F \in V \to \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\} \in V$
8	7	adantl	$⊢ (J \in V \land F \in V) \to \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\} \in V$
9		simpr	$⊢ (j = J \land f = F) \to f = F$
10		simpl	$⊢ (j = J \land f = F) \to j = J$
11	10	unieqd	$⊢ (j = J \land f = F) \to ⋃ j = ⋃ J$
12	11 1	eqtr4di	$⊢ (j = J \land f = F) \to ⋃ j = X$
13	9 12	imaeq12d	$⊢ (j = J \land f = F) \to f [⋃ j] = F [X]$
14	13	pweqd	$⊢ (j = J \land f = F) \to 𝒫 f [⋃ j] = 𝒫 F [X]$
15	9	cnveqd	$⊢ (j = J \land f = F) \to f^{-1} = F^{-1}$
16	15	imaeq1d	$⊢ (j = J \land f = F) \to f^{-1} [s] = F^{-1} [s]$
17	16 12	ineq12d	$⊢ (j = J \land f = F) \to f^{-1} [s] \cap ⋃ j = F^{-1} [s] \cap X$
18	17 10	eleq12d	$⊢ (j = J \land f = F) \to (f^{-1} [s] \cap ⋃ j \in j \leftrightarrow F^{-1} [s] \cap X \in J)$
19	14 18	rabeqbidv	$⊢ (j = J \land f = F) \to \{s \in 𝒫 f [⋃ j] \| f^{-1} [s] \cap ⋃ j \in j\} = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$
20		df-qtop	$⊢ qTop = (j \in V, f \in V ⟼ \{s \in 𝒫 f [⋃ j] \| f^{-1} [s] \cap ⋃ j \in j\})$
21	19 20	ovmpoga	$⊢ (J \in V \land F \in V \land \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\} \in V) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$
22	8 21	mpd3an3	$⊢ (J \in V \land F \in V) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$
23	2 3 22	syl2an	$⊢ (J \in V \land F \in W) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$

Metamath Proof Explorer

Theorem qtopval

Proof