Metamath Proof Explorer

Theorem cnt1

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

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

Proof

Step Hyp Ref Expression
1 cntop1 
 |-  ( F e. ( J Cn K ) -> J e. Top )
2 1 3ad2ant3 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Top )
3 eqid 
 |-  U. J = U. J
4 eqid 
 |-  U. K = U. K
5 3 4 cnf 
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
6 5 3ad2ant3 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> F : U. J --> U. K )
7 6 ffnd 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> F Fn U. J )
8 fnsnfv 
 |-  ( ( F Fn U. J /\ x e. U. J ) -> { ( F ` x ) } = ( F " { x } ) )
9 7 8 sylan 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> { ( F ` x ) } = ( F " { x } ) )
10 9 imaeq2d 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> ( `' F " { ( F ` x ) } ) = ( `' F " ( F " { x } ) ) )
11 simpl2 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> F : X -1-1-> Y )
12 6 fdmd 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> dom F = U. J )
13 f1dm 
 |-  ( F : X -1-1-> Y -> dom F = X )
14 13 3ad2ant2 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> dom F = X )
15 12 14 eqtr3d 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> U. J = X )
16 15 eleq2d 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> ( x e. U. J <-> x e. X ) )
17 16 biimpa 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> x e. X )
18 17 snssd 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> { x } C_ X )
19 f1imacnv 
 |-  ( ( F : X -1-1-> Y /\ { x } C_ X ) -> ( `' F " ( F " { x } ) ) = { x } )
20 11 18 19 syl2anc 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> ( `' F " ( F " { x } ) ) = { x } )
21 10 20 eqtrd 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> ( `' F " { ( F ` x ) } ) = { x } )
22 simpl3 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> F e. ( J Cn K ) )
23 simpl1 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> K e. Fre )
24 6 ffvelcdmda 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> ( F ` x ) e. U. K )
25 4 t1sncld 
 |-  ( ( K e. Fre /\ ( F ` x ) e. U. K ) -> { ( F ` x ) } e. ( Clsd ` K ) )
26 23 24 25 syl2anc 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> { ( F ` x ) } e. ( Clsd ` K ) )
27 cnclima 
 |-  ( ( F e. ( J Cn K ) /\ { ( F ` x ) } e. ( Clsd ` K ) ) -> ( `' F " { ( F ` x ) } ) e. ( Clsd ` J ) )
28 22 26 27 syl2anc 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> ( `' F " { ( F ` x ) } ) e. ( Clsd ` J ) )
29 21 28 eqeltrrd 
 |-  ( ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ x e. U. J ) -> { x } e. ( Clsd ` J ) )
30 29 ralrimiva 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> A. x e. U. J { x } e. ( Clsd ` J ) )
31 3 ist1 
 |-  ( J e. Fre <-> ( J e. Top /\ A. x e. U. J { x } e. ( Clsd ` J ) ) )
32 2 30 31 sylanbrc 
 |-  ( ( K e. Fre /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Fre )