Step |
Hyp |
Ref |
Expression |
1 |
|
hhlm.1 |
โข ๐ = โจ โจ +โ , ยทโ โฉ , normโ โฉ |
2 |
|
hhlm.2 |
โข ๐ท = ( IndMet โ ๐ ) |
3 |
|
hhlm.3 |
โข ๐ฝ = ( MetOpen โ ๐ท ) |
4 |
|
hhcmpl.c |
โข ( ๐น โ ( Cau โ ๐ท ) โ โ ๐ฅ โ โ ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) |
5 |
4
|
anim1ci |
โข ( ( ๐น โ ( Cau โ ๐ท ) โง ๐น โ ( โ โm โ ) ) โ ( ๐น โ ( โ โm โ ) โง โ ๐ฅ โ โ ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) ) |
6 |
|
elin |
โข ( ๐น โ ( ( Cau โ ๐ท ) โฉ ( โ โm โ ) ) โ ( ๐น โ ( Cau โ ๐ท ) โง ๐น โ ( โ โm โ ) ) ) |
7 |
|
r19.42v |
โข ( โ ๐ฅ โ โ ( ๐น โ ( โ โm โ ) โง ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) โ ( ๐น โ ( โ โm โ ) โง โ ๐ฅ โ โ ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) ) |
8 |
5 6 7
|
3imtr4i |
โข ( ๐น โ ( ( Cau โ ๐ท ) โฉ ( โ โm โ ) ) โ โ ๐ฅ โ โ ( ๐น โ ( โ โm โ ) โง ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) ) |
9 |
1 2
|
hhcau |
โข Cauchy = ( ( Cau โ ๐ท ) โฉ ( โ โm โ ) ) |
10 |
9
|
eleq2i |
โข ( ๐น โ Cauchy โ ๐น โ ( ( Cau โ ๐ท ) โฉ ( โ โm โ ) ) ) |
11 |
1 2 3
|
hhlm |
โข โ๐ฃ = ( ( โ๐ก โ ๐ฝ ) โพ ( โ โm โ ) ) |
12 |
11
|
breqi |
โข ( ๐น โ๐ฃ ๐ฅ โ ๐น ( ( โ๐ก โ ๐ฝ ) โพ ( โ โm โ ) ) ๐ฅ ) |
13 |
|
vex |
โข ๐ฅ โ V |
14 |
13
|
brresi |
โข ( ๐น ( ( โ๐ก โ ๐ฝ ) โพ ( โ โm โ ) ) ๐ฅ โ ( ๐น โ ( โ โm โ ) โง ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) ) |
15 |
12 14
|
bitri |
โข ( ๐น โ๐ฃ ๐ฅ โ ( ๐น โ ( โ โm โ ) โง ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) ) |
16 |
15
|
rexbii |
โข ( โ ๐ฅ โ โ ๐น โ๐ฃ ๐ฅ โ โ ๐ฅ โ โ ( ๐น โ ( โ โm โ ) โง ๐น ( โ๐ก โ ๐ฝ ) ๐ฅ ) ) |
17 |
8 10 16
|
3imtr4i |
โข ( ๐น โ Cauchy โ โ ๐ฅ โ โ ๐น โ๐ฃ ๐ฅ ) |