Metamath Proof Explorer

Theorem axhcompl-zf

Description: Derive Axiom ax-hcompl from Hilbert space under ZF set theory. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses axhil.1 
|- U = <. <. +h , .h >. , normh >.
axhil.2 
|- U e. CHilOLD
Assertion axhcompl-zf 
|- ( F e. Cauchy -> E. x e. ~H F ~~>v x )

Proof

Step Hyp Ref Expression
1 axhil.1 
 |-  U = <. <. +h , .h >. , normh >.
2 axhil.2 
 |-  U e. CHilOLD
3 simpl 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> F e. ( Cau ` ( IndMet ` U ) ) )
4 eqid 
 |-  ( IndMet ` U ) = ( IndMet ` U )
5 eqid 
 |-  ( MetOpen ` ( IndMet ` U ) ) = ( MetOpen ` ( IndMet ` U ) )
6 4 5 hlcompl 
 |-  ( ( U e. CHilOLD /\ F e. ( Cau ` ( IndMet ` U ) ) ) -> F e. dom ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) )
7 2 3 6 sylancr 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> F e. dom ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) )
8 eldm2g 
 |-  ( F e. ( Cau ` ( IndMet ` U ) ) -> ( F e. dom ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) <-> E. x <. F , x >. e. ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) ) )
9 8 adantr 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( F e. dom ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) <-> E. x <. F , x >. e. ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) ) )
10 7 9 mpbid 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> E. x <. F , x >. e. ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) )
11 df-br 
 |-  ( F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x <-> <. F , x >. e. ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) )
12 2 hlnvi 
 |-  U e. NrmCVec
13 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
14 1 fveq2i 
 |-  ( BaseSet ` U ) = ( BaseSet ` <. <. +h , .h >. , normh >. )
15 13 14 eqtr4i 
 |-  ~H = ( BaseSet ` U )
16 15 4 imsxmet 
 |-  ( U e. NrmCVec -> ( IndMet ` U ) e. ( *Met ` ~H ) )
17 5 mopntopon 
 |-  ( ( IndMet ` U ) e. ( *Met ` ~H ) -> ( MetOpen ` ( IndMet ` U ) ) e. ( TopOn ` ~H ) )
18 12 16 17 mp2b 
 |-  ( MetOpen ` ( IndMet ` U ) ) e. ( TopOn ` ~H )
19 lmcl 
 |-  ( ( ( MetOpen ` ( IndMet ` U ) ) e. ( TopOn ` ~H ) /\ F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x ) -> x e. ~H )
20 18 19 mpan 
 |-  ( F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x -> x e. ~H )
21 20 a1i 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x -> x e. ~H ) )
22 1 12 15 4 5 h2hlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) |` ( ~H ^m NN ) )
23 22 breqi 
 |-  ( F ~~>v x <-> F ( ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) |` ( ~H ^m NN ) ) x )
24 brres 
 |-  ( x e. _V -> ( F ( ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) |` ( ~H ^m NN ) ) x <-> ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x ) ) )
25 24 elv 
 |-  ( F ( ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) |` ( ~H ^m NN ) ) x <-> ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x ) )
26 23 25 bitri 
 |-  ( F ~~>v x <-> ( F e. ( ~H ^m NN ) /\ F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x ) )
27 26 baib 
 |-  ( F e. ( ~H ^m NN ) -> ( F ~~>v x <-> F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x ) )
28 27 adantl 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( F ~~>v x <-> F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x ) )
29 28 biimprd 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x -> F ~~>v x ) )
30 21 29 jcad 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( F ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) x -> ( x e. ~H /\ F ~~>v x ) ) )
31 11 30 syl5bir 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( <. F , x >. e. ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) -> ( x e. ~H /\ F ~~>v x ) ) )
32 31 eximdv 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> ( E. x <. F , x >. e. ( ~~>t ` ( MetOpen ` ( IndMet ` U ) ) ) -> E. x ( x e. ~H /\ F ~~>v x ) ) )
33 10 32 mpd 
 |-  ( ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) -> E. x ( x e. ~H /\ F ~~>v x ) )
34 elin 
 |-  ( F e. ( ( Cau ` ( IndMet ` U ) ) i^i ( ~H ^m NN ) ) <-> ( F e. ( Cau ` ( IndMet ` U ) ) /\ F e. ( ~H ^m NN ) ) )
35 df-rex 
 |-  ( E. x e. ~H F ~~>v x <-> E. x ( x e. ~H /\ F ~~>v x ) )
36 33 34 35 3imtr4i 
 |-  ( F e. ( ( Cau ` ( IndMet ` U ) ) i^i ( ~H ^m NN ) ) -> E. x e. ~H F ~~>v x )
37 1 12 15 4 h2hcau 
 |-  Cauchy = ( ( Cau ` ( IndMet ` U ) ) i^i ( ~H ^m NN ) )
38 36 37 eleq2s 
 |-  ( F e. Cauchy -> E. x e. ~H F ~~>v x )