Metamath Proof Explorer

Theorem ist0-4

Description: The topological indistinguishability map is injective iff the space is T_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion ist0-4 
|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F : X -1-1-> _V ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqfeq 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. y e. J ( z e. y <-> w e. y ) ) )
3 2 3expb 
 |-  ( ( J e. ( TopOn ` X ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) = ( F ` w ) <-> A. y e. J ( z e. y <-> w e. y ) ) )
4 3 imbi1d 
 |-  ( ( J e. ( TopOn ` X ) /\ ( z e. X /\ w e. X ) ) -> ( ( ( F ` z ) = ( F ` w ) -> z = w ) <-> ( A. y e. J ( z e. y <-> w e. y ) -> z = w ) ) )
5 4 2ralbidva 
 |-  ( J e. ( TopOn ` X ) -> ( A. z e. X A. w e. X ( ( F ` z ) = ( F ` w ) -> z = w ) <-> A. z e. X A. w e. X ( A. y e. J ( z e. y <-> w e. y ) -> z = w ) ) )
6 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
7 dffn2 
 |-  ( F Fn X <-> F : X --> _V )
8 6 7 sylib 
 |-  ( J e. ( TopOn ` X ) -> F : X --> _V )
9 dff13 
 |-  ( F : X -1-1-> _V <-> ( F : X --> _V /\ A. z e. X A. w e. X ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
10 9 baib 
 |-  ( F : X --> _V -> ( F : X -1-1-> _V <-> A. z e. X A. w e. X ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
11 8 10 syl 
 |-  ( J e. ( TopOn ` X ) -> ( F : X -1-1-> _V <-> A. z e. X A. w e. X ( ( F ` z ) = ( F ` w ) -> z = w ) ) )
12 ist0-2 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> A. z e. X A. w e. X ( A. y e. J ( z e. y <-> w e. y ) -> z = w ) ) )
13 5 11 12 3bitr4rd 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F : X -1-1-> _V ) )