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 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion kqsat 
|- ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( `' F " ( F " U ) ) = U )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
3 elpreima 
 |-  ( F Fn X -> ( z e. ( `' F " ( F " U ) ) <-> ( z e. X /\ ( F ` z ) e. ( F " U ) ) ) )
4 2 3 syl 
 |-  ( J e. ( TopOn ` X ) -> ( z e. ( `' F " ( F " U ) ) <-> ( z e. X /\ ( F ` z ) e. ( F " U ) ) ) )
5 4 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( z e. ( `' F " ( F " U ) ) <-> ( z e. X /\ ( F ` z ) e. ( F " U ) ) ) )
6 1 kqfvima 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ z e. X ) -> ( z e. U <-> ( F ` z ) e. ( F " U ) ) )
7 6 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ z e. X ) -> ( z e. U <-> ( F ` z ) e. ( F " U ) ) )
8 7 biimprd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J ) /\ z e. X ) -> ( ( F ` z ) e. ( F " U ) -> z e. U ) )
9 8 expimpd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( ( z e. X /\ ( F ` z ) e. ( F " U ) ) -> z e. U ) )
10 5 9 sylbid 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( z e. ( `' F " ( F " U ) ) -> z e. U ) )
11 10 ssrdv 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( `' F " ( F " U ) ) C_ U )
12 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> U C_ X )
13 2 fndmd 
 |-  ( J e. ( TopOn ` X ) -> dom F = X )
14 13 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> dom F = X )
15 12 14 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> U C_ dom F )
16 sseqin2 
 |-  ( U C_ dom F <-> ( dom F i^i U ) = U )
17 15 16 sylib 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( dom F i^i U ) = U )
18 dminss 
 |-  ( dom F i^i U ) C_ ( `' F " ( F " U ) )
19 17 18 eqsstrrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> U C_ ( `' F " ( F " U ) ) )
20 11 19 eqssd 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> ( `' F " ( F " U ) ) = U )