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 )