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 )