Metamath Proof Explorer


Theorem hhcmpl

Description: Lemma used for derivation of the completeness axiom ax-hcompl from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

Ref Expression
Hypotheses hhlm.1 โŠข ๐‘ˆ = โŸจ โŸจ +โ„Ž , ยทโ„Ž โŸฉ , normโ„Ž โŸฉ
hhlm.2 โŠข ๐ท = ( IndMet โ€˜ ๐‘ˆ )
hhlm.3 โŠข ๐ฝ = ( MetOpen โ€˜ ๐ท )
hhcmpl.c โŠข ( ๐น โˆˆ ( Cau โ€˜ ๐ท ) โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‹ ๐น ( โ‡๐‘ก โ€˜ ๐ฝ ) ๐‘ฅ )
Assertion hhcmpl ( ๐น โˆˆ Cauchy โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‹ ๐น โ‡๐‘ฃ ๐‘ฅ )

Proof

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 โ†’ โˆƒ ๐‘ฅ โˆˆ โ„‹ ๐น โ‡๐‘ฃ ๐‘ฅ )