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 𝑈 = ⟨ ⟨ + , · ⟩ , norm
axhil.2 𝑈 ∈ CHilOLD
Assertion axhcompl-zf ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹𝑣 𝑥 )

Proof

Step Hyp Ref Expression
1 axhil.1 𝑈 = ⟨ ⟨ + , · ⟩ , norm
2 axhil.2 𝑈 ∈ CHilOLD
3 simpl ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) )
4 eqid ( IndMet ‘ 𝑈 ) = ( IndMet ‘ 𝑈 )
5 eqid ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) = ( MetOpen ‘ ( IndMet ‘ 𝑈 ) )
6 4 5 hlcompl ( ( 𝑈 ∈ CHilOLD𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
7 2 3 6 sylancr ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
8 eldm2g ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) → ( 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ↔ ∃ 𝑥𝐹 , 𝑥 ⟩ ∈ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ) )
9 8 adantr ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( 𝐹 ∈ dom ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ↔ ∃ 𝑥𝐹 , 𝑥 ⟩ ∈ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ) )
10 7 9 mpbid ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ∃ 𝑥𝐹 , 𝑥 ⟩ ∈ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
11 df-br ( 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ↔ ⟨ 𝐹 , 𝑥 ⟩ ∈ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) )
12 2 hlnvi 𝑈 ∈ NrmCVec
13 df-hba ℋ = ( BaseSet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
14 1 fveq2i ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ ⟨ ⟨ + , · ⟩ , norm ⟩ )
15 13 14 eqtr4i ℋ = ( BaseSet ‘ 𝑈 )
16 15 4 imsxmet ( 𝑈 ∈ NrmCVec → ( IndMet ‘ 𝑈 ) ∈ ( ∞Met ‘ ℋ ) )
17 5 mopntopon ( ( IndMet ‘ 𝑈 ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ∈ ( TopOn ‘ ℋ ) )
18 12 16 17 mp2b ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ∈ ( TopOn ‘ ℋ )
19 lmcl ( ( ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ∈ ( TopOn ‘ ℋ ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ) → 𝑥 ∈ ℋ )
20 18 19 mpan ( 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥𝑥 ∈ ℋ )
21 20 a1i ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥𝑥 ∈ ℋ ) )
22 1 12 15 4 5 h2hlm 𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ↾ ( ℋ ↑m ℕ ) )
23 22 breqi ( 𝐹𝑣 𝑥𝐹 ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 )
24 brres ( 𝑥 ∈ V → ( 𝐹 ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ) ) )
25 24 elv ( 𝐹 ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) ↾ ( ℋ ↑m ℕ ) ) 𝑥 ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ) )
26 23 25 bitri ( 𝐹𝑣 𝑥 ↔ ( 𝐹 ∈ ( ℋ ↑m ℕ ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ) )
27 26 baib ( 𝐹 ∈ ( ℋ ↑m ℕ ) → ( 𝐹𝑣 𝑥𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ) )
28 27 adantl ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( 𝐹𝑣 𝑥𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 ) )
29 28 biimprd ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥𝐹𝑣 𝑥 ) )
30 21 29 jcad ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) 𝑥 → ( 𝑥 ∈ ℋ ∧ 𝐹𝑣 𝑥 ) ) )
31 11 30 syl5bir ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( ⟨ 𝐹 , 𝑥 ⟩ ∈ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) → ( 𝑥 ∈ ℋ ∧ 𝐹𝑣 𝑥 ) ) )
32 31 eximdv ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ( ∃ 𝑥𝐹 , 𝑥 ⟩ ∈ ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 𝑈 ) ) ) → ∃ 𝑥 ( 𝑥 ∈ ℋ ∧ 𝐹𝑣 𝑥 ) ) )
33 10 32 mpd ( ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) → ∃ 𝑥 ( 𝑥 ∈ ℋ ∧ 𝐹𝑣 𝑥 ) )
34 elin ( 𝐹 ∈ ( ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∩ ( ℋ ↑m ℕ ) ) ↔ ( 𝐹 ∈ ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∧ 𝐹 ∈ ( ℋ ↑m ℕ ) ) )
35 df-rex ( ∃ 𝑥 ∈ ℋ 𝐹𝑣 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ ℋ ∧ 𝐹𝑣 𝑥 ) )
36 33 34 35 3imtr4i ( 𝐹 ∈ ( ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∩ ( ℋ ↑m ℕ ) ) → ∃ 𝑥 ∈ ℋ 𝐹𝑣 𝑥 )
37 1 12 15 4 h2hcau Cauchy = ( ( Cau ‘ ( IndMet ‘ 𝑈 ) ) ∩ ( ℋ ↑m ℕ ) )
38 36 37 eleq2s ( 𝐹 ∈ Cauchy → ∃ 𝑥 ∈ ℋ 𝐹𝑣 𝑥 )