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 biimtrrid ⊢ ( ( 𝐹 ∈ ( 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 → ∃ 𝑥 ∈ ℋ 𝐹 ⇝𝑣 𝑥 )