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 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion kqsat ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F -1 F U = U

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 1 kqffn ⊢ J ∈ TopOn ⁡ X → F Fn X
3 elpreima ⊢ F Fn X → z ∈ F -1 F U ↔ z ∈ X ∧ F ⁡ z ∈ F U
4 2 3 syl ⊢ J ∈ TopOn ⁡ X → z ∈ F -1 F U ↔ z ∈ X ∧ F ⁡ z ∈ F U
5 4 adantr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → z ∈ F -1 F U ↔ z ∈ X ∧ F ⁡ z ∈ F U
6 1 kqfvima ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ z ∈ X → z ∈ U ↔ F ⁡ z ∈ F U
7 6 3expa ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ z ∈ X → z ∈ U ↔ F ⁡ z ∈ F U
8 7 biimprd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J ∧ z ∈ X → F ⁡ z ∈ F U → z ∈ U
9 8 expimpd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → z ∈ X ∧ F ⁡ z ∈ F U → z ∈ U
10 5 9 sylbid ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → z ∈ F -1 F U → z ∈ U
11 10 ssrdv ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F -1 F U ⊆ U
12 toponss ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → U ⊆ X
13 2 fndmd ⊢ J ∈ TopOn ⁡ X → dom ⁡ F = X
14 13 adantr ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → dom ⁡ F = X
15 12 14 sseqtrrd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → U ⊆ dom ⁡ F
16 sseqin2 ⊢ U ⊆ dom ⁡ F ↔ dom ⁡ F ∩ U = U
17 15 16 sylib ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → dom ⁡ F ∩ U = U
18 dminss ⊢ dom ⁡ F ∩ U ⊆ F -1 F U
19 17 18 eqsstrrdi ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → U ⊆ F -1 F U
20 11 19 eqssd ⊢ J ∈ TopOn ⁡ X ∧ U ∈ J → F -1 F U = U