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 ) |