Metamath Proof Explorer

Theorem cnt0

Description: The preimage of a T_0 topology under an injective map is T_0. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion cnt0 
|- ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Kol2 )

Proof

Step Hyp Ref Expression
1 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
2 1 3ad2ant3 
 |-  ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Top )
3 simpl3 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> F e. ( J Cn K ) )
4 cnima 
 |-  ( ( F e. ( J Cn K ) /\ w e. K ) -> ( `' F " w ) e. J )
5 3 4 sylan 
 |-  ( ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) /\ w e. K ) -> ( `' F " w ) e. J )
6 eleq2 
 |-  ( z = ( `' F " w ) -> ( x e. z <-> x e. ( `' F " w ) ) )
7 eleq2 
 |-  ( z = ( `' F " w ) -> ( y e. z <-> y e. ( `' F " w ) ) )
8 6 7 bibi12d 
 |-  ( z = ( `' F " w ) -> ( ( x e. z <-> y e. z ) <-> ( x e. ( `' F " w ) <-> y e. ( `' F " w ) ) ) )
9 8 rspcv 
 |-  ( ( `' F " w ) e. J -> ( A. z e. J ( x e. z <-> y e. z ) -> ( x e. ( `' F " w ) <-> y e. ( `' F " w ) ) ) )
10 5 9 syl 
 |-  ( ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) /\ w e. K ) -> ( A. z e. J ( x e. z <-> y e. z ) -> ( x e. ( `' F " w ) <-> y e. ( `' F " w ) ) ) )
11 simprl 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> x e. U. J )
12 eqid 
 |-  U. J = U. J
13 eqid 
 |-  U. K = U. K
14 12 13 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
15 3 14 syl 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> F : U. J --> U. K )
16 15 ffnd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> F Fn U. J )
17 elpreima 
 |-  ( F Fn U. J -> ( x e. ( `' F " w ) <-> ( x e. U. J /\ ( F ` x ) e. w ) ) )
18 16 17 syl 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( x e. ( `' F " w ) <-> ( x e. U. J /\ ( F ` x ) e. w ) ) )
19 11 18 mpbirand 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( x e. ( `' F " w ) <-> ( F ` x ) e. w ) )
20 simprr 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> y e. U. J )
21 elpreima 
 |-  ( F Fn U. J -> ( y e. ( `' F " w ) <-> ( y e. U. J /\ ( F ` y ) e. w ) ) )
22 16 21 syl 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( y e. ( `' F " w ) <-> ( y e. U. J /\ ( F ` y ) e. w ) ) )
23 20 22 mpbirand 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( y e. ( `' F " w ) <-> ( F ` y ) e. w ) )
24 19 23 bibi12d 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( ( x e. ( `' F " w ) <-> y e. ( `' F " w ) ) <-> ( ( F ` x ) e. w <-> ( F ` y ) e. w ) ) )
25 24 adantr 
 |-  ( ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) /\ w e. K ) -> ( ( x e. ( `' F " w ) <-> y e. ( `' F " w ) ) <-> ( ( F ` x ) e. w <-> ( F ` y ) e. w ) ) )
26 10 25 sylibd 
 |-  ( ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) /\ w e. K ) -> ( A. z e. J ( x e. z <-> y e. z ) -> ( ( F ` x ) e. w <-> ( F ` y ) e. w ) ) )
27 26 ralrimdva 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( A. z e. J ( x e. z <-> y e. z ) -> A. w e. K ( ( F ` x ) e. w <-> ( F ` y ) e. w ) ) )
28 simpl1 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> K e. Kol2 )
29 15 11 ffvelrnd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( F ` x ) e. U. K )
30 15 20 ffvelrnd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( F ` y ) e. U. K )
31 13 t0sep 
 |-  ( ( K e. Kol2 /\ ( ( F ` x ) e. U. K /\ ( F ` y ) e. U. K ) ) -> ( A. w e. K ( ( F ` x ) e. w <-> ( F ` y ) e. w ) -> ( F ` x ) = ( F ` y ) ) )
32 28 29 30 31 syl12anc 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( A. w e. K ( ( F ` x ) e. w <-> ( F ` y ) e. w ) -> ( F ` x ) = ( F ` y ) ) )
33 27 32 syld 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( A. z e. J ( x e. z <-> y e. z ) -> ( F ` x ) = ( F ` y ) ) )
34 simpl2 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> F : X -1-1-> Y )
35 15 fdmd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> dom F = U. J )
36 f1dm 
 |-  ( F : X -1-1-> Y -> dom F = X )
37 34 36 syl 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> dom F = X )
38 35 37 eqtr3d 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> U. J = X )
39 11 38 eleqtrd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> x e. X )
40 20 38 eleqtrd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> y e. X )
41 f1fveq 
 |-  ( ( F : X -1-1-> Y /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
42 34 39 40 41 syl12anc 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
43 33 42 sylibd 
 |-  ( ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) )
44 43 ralrimivva 
 |-  ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> A. x e. U. J A. y e. U. J ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) )
45 12 ist0 
 |-  ( J e. Kol2 <-> ( J e. Top /\ A. x e. U. J A. y e. U. J ( A. z e. J ( x e. z <-> y e. z ) -> x = y ) ) )
46 2 44 45 sylanbrc 
 |-  ( ( K e. Kol2 /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Kol2 )