This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑋 ) ∧ 𝑈 ∈ 𝐽 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑈 ) ) = 𝑈 )