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 = + ℎ ⋅ ℎ norm ℎ
axhil.2 ⊢ U ∈ CHil OLD
Assertion axhcompl-zf ⊢ F ∈ Cauchy → ∃ x ∈ ℋ F ⇝v x

Proof

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