Theorem kqval

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

	Ref	Expression
Hypothesis	kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
Assertion	kqval	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2		topontop	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
3		id	⊢ ( 𝑗 = 𝐽 → 𝑗 = 𝐽 )
4		unieq	⊢ ( 𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽 )
5		rabeq	⊢ ( 𝑗 = 𝐽 → { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } = { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
6	4 5	mpteq12dv	⊢ ( 𝑗 = 𝐽 → ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) )
7	3 6	oveq12d	⊢ ( 𝑗 = 𝐽 → ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
8		df-kq	⊢ KQ = ( 𝑗 ∈ Top ↦ ( 𝑗 qTop ( 𝑥 ∈ ∪ 𝑗 ↦ { 𝑦 ∈ 𝑗 ∣ 𝑥 ∈ 𝑦 } ) ) )
9		ovex	⊢ ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝐽 ∈ Top → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
11	2 10	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
12		toponuni	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
13	12	mpteq1d	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) )
14	1 13	syl5eq	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 = ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) )
15	14	oveq2d	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 qTop 𝐹 ) = ( 𝐽 qTop ( 𝑥 ∈ ∪ 𝐽 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) ) )
16	11 15	eqtr4d	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )