Description: The topological indistinguishability map is a continuous function into the Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | kqval.2 | ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) | |
Assertion | kqid | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | kqval.2 | ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } ) | |
2 | 1 | kqffn | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 ) |
3 | qtopid | ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) | |
4 | 2 3 | mpdan | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) |
5 | 1 | kqval | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) ) |
6 | 5 | oveq2d | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) = ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) ) |
7 | 4 6 | eleqtrrd | ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( KQ ‘ 𝐽 ) ) ) |