Theorem kqsat

Description: Any open set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest ). (Contributed by Mario Carneiro, 25-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		kqval.2	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦 } )
2	1	kqffn	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐹 Fn 𝑋 )
3		elpreima	⊢ ( 𝐹 Fn 𝑋 → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
4	2 3	syl	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
5	4	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ↔ ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) ) )
6	1	kqfvima	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) )
7	6	3expa	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑈 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) )
8	7	biimprd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) → 𝑧 ∈ 𝑈 ) )
9	8	expimpd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝑧 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) )
10	5 9	sylbid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) → 𝑧 ∈ 𝑈 ) )
11	10	ssrdv	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) ⊆ 𝑈 )
12		toponss	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ 𝑋 )
13	2	fndmd	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → dom 𝐹 = 𝑋 )
14	13	adantr	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → dom 𝐹 = 𝑋 )
15	12 14	sseqtrrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ dom 𝐹 )
16		sseqin2	⊢ ( 𝑈 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑈 ) = 𝑈 )
17	15 16	sylib	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( dom 𝐹 ∩ 𝑈 ) = 𝑈 )
18		dminss	⊢ ( dom 𝐹 ∩ 𝑈 ) ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) )
19	17 18	eqsstrrdi	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → 𝑈 ⊆ ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) )
20	11 19	eqssd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) = 𝑈 )