kqval

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

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqval	$⊢ J \in TopOn (X) \to KQ (J) = J qTop F$

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2		topontop	$⊢ J \in TopOn (X) \to J \in Top$
3		id	$⊢ j = J \to j = J$
4		unieq	$⊢ j = J \to ⋃ j = ⋃ J$
5		rabeq	$⊢ j = J \to \{y \in j \| x \in y\} = \{y \in J \| x \in y\}$
6	4 5	mpteq12dv	$⊢ j = J \to (x \in ⋃ j ⟼ \{y \in j \| x \in y\}) = (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
7	3 6	oveq12d	$⊢ j = J \to j qTop (x \in ⋃ j ⟼ \{y \in j \| x \in y\}) = J qTop (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
8		df-kq	$⊢ KQ = (j \in Top ⟼ j qTop (x \in ⋃ j ⟼ \{y \in j \| x \in y\}))$
9		ovex	$⊢ J qTop (x \in ⋃ J ⟼ \{y \in J \| x \in y\}) \in V$
10	7 8 9	fvmpt	$⊢ J \in Top \to KQ (J) = J qTop (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
11	2 10	syl	$⊢ J \in TopOn (X) \to KQ (J) = J qTop (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
12		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
13	12	mpteq1d	$⊢ J \in TopOn (X) \to (x \in X ⟼ \{y \in J \| x \in y\}) = (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
14	1 13	eqtrid	$⊢ J \in TopOn (X) \to F = (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
15	14	oveq2d	$⊢ J \in TopOn (X) \to J qTop F = J qTop (x \in ⋃ J ⟼ \{y \in J \| x \in y\})$
16	11 15	eqtr4d	$⊢ J \in TopOn (X) \to KQ (J) = J qTop F$

Metamath Proof Explorer