Metamath Proof Explorer


Theorem cnhaus

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

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

Proof

Step Hyp Ref Expression
1 cntop1
 |-  ( F e. ( J Cn K ) -> J e. Top )
2 1 3ad2ant3
 |-  ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Top )
3 simpl1
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> K e. Haus )
4 simpl3
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> F e. ( J Cn K ) )
5 eqid
 |-  U. J = U. J
6 eqid
 |-  U. K = U. K
7 5 6 cnf
 |-  ( F e. ( J Cn K ) -> F : U. J --> U. K )
8 4 7 syl
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> F : U. J --> U. K )
9 simprll
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> x e. U. J )
10 8 9 ffvelrnd
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> ( F ` x ) e. U. K )
11 simprlr
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> y e. U. J )
12 8 11 ffvelrnd
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> ( F ` y ) e. U. K )
13 simprr
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> x =/= y )
14 simpl2
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> F : X -1-1-> Y )
15 8 fdmd
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> dom F = U. J )
16 f1dm
 |-  ( F : X -1-1-> Y -> dom F = X )
17 14 16 syl
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> dom F = X )
18 15 17 eqtr3d
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> U. J = X )
19 9 18 eleqtrd
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> x e. X )
20 11 18 eleqtrd
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> y e. X )
21 f1fveq
 |-  ( ( F : X -1-1-> Y /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
22 14 19 20 21 syl12anc
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> ( ( F ` x ) = ( F ` y ) <-> x = y ) )
23 22 necon3bid
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> ( ( F ` x ) =/= ( F ` y ) <-> x =/= y ) )
24 13 23 mpbird
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> ( F ` x ) =/= ( F ` y ) )
25 6 hausnei
 |-  ( ( K e. Haus /\ ( ( F ` x ) e. U. K /\ ( F ` y ) e. U. K /\ ( F ` x ) =/= ( F ` y ) ) ) -> E. u e. K E. v e. K ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) )
26 3 10 12 24 25 syl13anc
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> E. u e. K E. v e. K ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) )
27 simpll3
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> F e. ( J Cn K ) )
28 simprll
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> u e. K )
29 cnima
 |-  ( ( F e. ( J Cn K ) /\ u e. K ) -> ( `' F " u ) e. J )
30 27 28 29 syl2anc
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( `' F " u ) e. J )
31 simprlr
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> v e. K )
32 cnima
 |-  ( ( F e. ( J Cn K ) /\ v e. K ) -> ( `' F " v ) e. J )
33 27 31 32 syl2anc
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( `' F " v ) e. J )
34 9 adantr
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> x e. U. J )
35 simprr1
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( F ` x ) e. u )
36 8 adantr
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> F : U. J --> U. K )
37 36 ffnd
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> F Fn U. J )
38 elpreima
 |-  ( F Fn U. J -> ( x e. ( `' F " u ) <-> ( x e. U. J /\ ( F ` x ) e. u ) ) )
39 37 38 syl
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( x e. ( `' F " u ) <-> ( x e. U. J /\ ( F ` x ) e. u ) ) )
40 34 35 39 mpbir2and
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> x e. ( `' F " u ) )
41 11 adantr
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> y e. U. J )
42 simprr2
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( F ` y ) e. v )
43 elpreima
 |-  ( F Fn U. J -> ( y e. ( `' F " v ) <-> ( y e. U. J /\ ( F ` y ) e. v ) ) )
44 37 43 syl
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( y e. ( `' F " v ) <-> ( y e. U. J /\ ( F ` y ) e. v ) ) )
45 41 42 44 mpbir2and
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> y e. ( `' F " v ) )
46 ffun
 |-  ( F : U. J --> U. K -> Fun F )
47 inpreima
 |-  ( Fun F -> ( `' F " ( u i^i v ) ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
48 36 46 47 3syl
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( `' F " ( u i^i v ) ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
49 simprr3
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( u i^i v ) = (/) )
50 49 imaeq2d
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( `' F " ( u i^i v ) ) = ( `' F " (/) ) )
51 ima0
 |-  ( `' F " (/) ) = (/)
52 50 51 eqtrdi
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( `' F " ( u i^i v ) ) = (/) )
53 48 52 eqtr3d
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> ( ( `' F " u ) i^i ( `' F " v ) ) = (/) )
54 eleq2
 |-  ( m = ( `' F " u ) -> ( x e. m <-> x e. ( `' F " u ) ) )
55 ineq1
 |-  ( m = ( `' F " u ) -> ( m i^i n ) = ( ( `' F " u ) i^i n ) )
56 55 eqeq1d
 |-  ( m = ( `' F " u ) -> ( ( m i^i n ) = (/) <-> ( ( `' F " u ) i^i n ) = (/) ) )
57 54 56 3anbi13d
 |-  ( m = ( `' F " u ) -> ( ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) <-> ( x e. ( `' F " u ) /\ y e. n /\ ( ( `' F " u ) i^i n ) = (/) ) ) )
58 eleq2
 |-  ( n = ( `' F " v ) -> ( y e. n <-> y e. ( `' F " v ) ) )
59 ineq2
 |-  ( n = ( `' F " v ) -> ( ( `' F " u ) i^i n ) = ( ( `' F " u ) i^i ( `' F " v ) ) )
60 59 eqeq1d
 |-  ( n = ( `' F " v ) -> ( ( ( `' F " u ) i^i n ) = (/) <-> ( ( `' F " u ) i^i ( `' F " v ) ) = (/) ) )
61 58 60 3anbi23d
 |-  ( n = ( `' F " v ) -> ( ( x e. ( `' F " u ) /\ y e. n /\ ( ( `' F " u ) i^i n ) = (/) ) <-> ( x e. ( `' F " u ) /\ y e. ( `' F " v ) /\ ( ( `' F " u ) i^i ( `' F " v ) ) = (/) ) ) )
62 57 61 rspc2ev
 |-  ( ( ( `' F " u ) e. J /\ ( `' F " v ) e. J /\ ( x e. ( `' F " u ) /\ y e. ( `' F " v ) /\ ( ( `' F " u ) i^i ( `' F " v ) ) = (/) ) ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
63 30 33 40 45 53 62 syl113anc
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( ( u e. K /\ v e. K ) /\ ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) ) ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
64 63 expr
 |-  ( ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) /\ ( u e. K /\ v e. K ) ) -> ( ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
65 64 rexlimdvva
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> ( E. u e. K E. v e. K ( ( F ` x ) e. u /\ ( F ` y ) e. v /\ ( u i^i v ) = (/) ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
66 26 65 mpd
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( ( x e. U. J /\ y e. U. J ) /\ x =/= y ) ) -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) )
67 66 expr
 |-  ( ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) /\ ( x e. U. J /\ y e. U. J ) ) -> ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
68 67 ralrimivva
 |-  ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> A. x e. U. J A. y e. U. J ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) )
69 5 ishaus
 |-  ( J e. Haus <-> ( J e. Top /\ A. x e. U. J A. y e. U. J ( x =/= y -> E. m e. J E. n e. J ( x e. m /\ y e. n /\ ( m i^i n ) = (/) ) ) ) )
70 2 68 69 sylanbrc
 |-  ( ( K e. Haus /\ F : X -1-1-> Y /\ F e. ( J Cn K ) ) -> J e. Haus )