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