Theorem kqopn

Description: The topological indistinguishability map is an open map. (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2		imassrn	⊢ ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹
3	2	a1i	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 )
4	1	kqsat	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) = 𝑈 )
5		simpr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ∈ 𝐽 )
6	4 5	eqeltrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ 𝐽 )
7	1	kqffn	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
8		dffn4	⊢ ( 𝐹 Fn 𝑋 ↔ 𝐹 : 𝑋 –onto→ ran 𝐹 )
9	7 8	sylib	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
10	9	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝐹 : 𝑋 –onto→ ran 𝐹 )
11		elqtop3	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ ran 𝐹 ) → ( ( 𝐹 “ 𝑈 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ 𝐽 ) ) )
12	10 11	syldan	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝐹 “ 𝑈 ) ∈ ( 𝐽 qTop 𝐹 ) ↔ ( ( 𝐹 “ 𝑈 ) ⊆ ran 𝐹 ∧ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ∈ 𝐽 ) ) )
13	3 6 12	mpbir2and	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ 𝑈 ) ∈ ( 𝐽 qTop 𝐹 ) )
14	1	kqval	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )
15	14	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( KQ ‘ 𝐽 ) = ( 𝐽 qTop 𝐹 ) )
16	13 15	eleqtrrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝐹 “ 𝑈 ) ∈ ( KQ ‘ 𝐽 ) )