Step |
Hyp |
Ref |
Expression |
1 |
|
hauseqlcld.k |
|- ( ph -> K e. Haus ) |
2 |
|
hauseqlcld.f |
|- ( ph -> F e. ( J Cn K ) ) |
3 |
|
hauseqlcld.g |
|- ( ph -> G e. ( J Cn K ) ) |
4 |
|
eqid |
|- U. J = U. J |
5 |
|
eqid |
|- U. K = U. K |
6 |
4 5
|
cnf |
|- ( F e. ( J Cn K ) -> F : U. J --> U. K ) |
7 |
2 6
|
syl |
|- ( ph -> F : U. J --> U. K ) |
8 |
7
|
ffvelrnda |
|- ( ( ph /\ b e. U. J ) -> ( F ` b ) e. U. K ) |
9 |
8
|
biantrurd |
|- ( ( ph /\ b e. U. J ) -> ( <. ( F ` b ) , ( G ` b ) >. e. _I <-> ( ( F ` b ) e. U. K /\ <. ( F ` b ) , ( G ` b ) >. e. _I ) ) ) |
10 |
|
fvex |
|- ( G ` b ) e. _V |
11 |
10
|
ideq |
|- ( ( F ` b ) _I ( G ` b ) <-> ( F ` b ) = ( G ` b ) ) |
12 |
|
df-br |
|- ( ( F ` b ) _I ( G ` b ) <-> <. ( F ` b ) , ( G ` b ) >. e. _I ) |
13 |
11 12
|
bitr3i |
|- ( ( F ` b ) = ( G ` b ) <-> <. ( F ` b ) , ( G ` b ) >. e. _I ) |
14 |
10
|
opelresi |
|- ( <. ( F ` b ) , ( G ` b ) >. e. ( _I |` U. K ) <-> ( ( F ` b ) e. U. K /\ <. ( F ` b ) , ( G ` b ) >. e. _I ) ) |
15 |
9 13 14
|
3bitr4g |
|- ( ( ph /\ b e. U. J ) -> ( ( F ` b ) = ( G ` b ) <-> <. ( F ` b ) , ( G ` b ) >. e. ( _I |` U. K ) ) ) |
16 |
|
fveq2 |
|- ( a = b -> ( F ` a ) = ( F ` b ) ) |
17 |
|
fveq2 |
|- ( a = b -> ( G ` a ) = ( G ` b ) ) |
18 |
16 17
|
opeq12d |
|- ( a = b -> <. ( F ` a ) , ( G ` a ) >. = <. ( F ` b ) , ( G ` b ) >. ) |
19 |
|
eqid |
|- ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) = ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) |
20 |
|
opex |
|- <. ( F ` b ) , ( G ` b ) >. e. _V |
21 |
18 19 20
|
fvmpt |
|- ( b e. U. J -> ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) = <. ( F ` b ) , ( G ` b ) >. ) |
22 |
21
|
adantl |
|- ( ( ph /\ b e. U. J ) -> ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) = <. ( F ` b ) , ( G ` b ) >. ) |
23 |
22
|
eleq1d |
|- ( ( ph /\ b e. U. J ) -> ( ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) <-> <. ( F ` b ) , ( G ` b ) >. e. ( _I |` U. K ) ) ) |
24 |
15 23
|
bitr4d |
|- ( ( ph /\ b e. U. J ) -> ( ( F ` b ) = ( G ` b ) <-> ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) |
25 |
24
|
pm5.32da |
|- ( ph -> ( ( b e. U. J /\ ( F ` b ) = ( G ` b ) ) <-> ( b e. U. J /\ ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) ) |
26 |
7
|
ffnd |
|- ( ph -> F Fn U. J ) |
27 |
4 5
|
cnf |
|- ( G e. ( J Cn K ) -> G : U. J --> U. K ) |
28 |
3 27
|
syl |
|- ( ph -> G : U. J --> U. K ) |
29 |
28
|
ffnd |
|- ( ph -> G Fn U. J ) |
30 |
|
fndmin |
|- ( ( F Fn U. J /\ G Fn U. J ) -> dom ( F i^i G ) = { b e. U. J | ( F ` b ) = ( G ` b ) } ) |
31 |
26 29 30
|
syl2anc |
|- ( ph -> dom ( F i^i G ) = { b e. U. J | ( F ` b ) = ( G ` b ) } ) |
32 |
31
|
eleq2d |
|- ( ph -> ( b e. dom ( F i^i G ) <-> b e. { b e. U. J | ( F ` b ) = ( G ` b ) } ) ) |
33 |
|
rabid |
|- ( b e. { b e. U. J | ( F ` b ) = ( G ` b ) } <-> ( b e. U. J /\ ( F ` b ) = ( G ` b ) ) ) |
34 |
32 33
|
bitrdi |
|- ( ph -> ( b e. dom ( F i^i G ) <-> ( b e. U. J /\ ( F ` b ) = ( G ` b ) ) ) ) |
35 |
|
opex |
|- <. ( F ` a ) , ( G ` a ) >. e. _V |
36 |
35 19
|
fnmpti |
|- ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) Fn U. J |
37 |
|
elpreima |
|- ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) Fn U. J -> ( b e. ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) <-> ( b e. U. J /\ ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) ) |
38 |
36 37
|
mp1i |
|- ( ph -> ( b e. ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) <-> ( b e. U. J /\ ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) ` b ) e. ( _I |` U. K ) ) ) ) |
39 |
25 34 38
|
3bitr4d |
|- ( ph -> ( b e. dom ( F i^i G ) <-> b e. ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) ) ) |
40 |
39
|
eqrdv |
|- ( ph -> dom ( F i^i G ) = ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) ) |
41 |
4 19
|
txcnmpt |
|- ( ( F e. ( J Cn K ) /\ G e. ( J Cn K ) ) -> ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) e. ( J Cn ( K tX K ) ) ) |
42 |
2 3 41
|
syl2anc |
|- ( ph -> ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) e. ( J Cn ( K tX K ) ) ) |
43 |
5
|
hausdiag |
|- ( K e. Haus <-> ( K e. Top /\ ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) ) ) |
44 |
43
|
simprbi |
|- ( K e. Haus -> ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) ) |
45 |
1 44
|
syl |
|- ( ph -> ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) ) |
46 |
|
cnclima |
|- ( ( ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) e. ( J Cn ( K tX K ) ) /\ ( _I |` U. K ) e. ( Clsd ` ( K tX K ) ) ) -> ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) e. ( Clsd ` J ) ) |
47 |
42 45 46
|
syl2anc |
|- ( ph -> ( `' ( a e. U. J |-> <. ( F ` a ) , ( G ` a ) >. ) " ( _I |` U. K ) ) e. ( Clsd ` J ) ) |
48 |
40 47
|
eqeltrd |
|- ( ph -> dom ( F i^i G ) e. ( Clsd ` J ) ) |