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=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
Assertion	axhcompl-zf	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$

Proof

Step	Hyp	Ref	Expression
1		axhil.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
3		simpl	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)$$
4		eqid	$$⊢\mathrm{IndMet}\left(U\right)=\mathrm{IndMet}\left(U\right)$$
5		eqid	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)=\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)$$
6	4 5	hlcompl	$$⊢\left(U\in {CHil}_{\mathrm{OLD}}\wedge F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\right)\to F\in \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)$$
7	2 3 6	sylancr	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to F\in \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)$$
8		eldm2g	$$⊢F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\to \left(F\in \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\leftrightarrow \exists x⟨F,x⟩\in \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\right)$$
9	8	adantr	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(F\in \mathrm{dom}\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\leftrightarrow \exists x⟨F,x⟩\in \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\right)$$
10	7 9	mpbid	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \exists x⟨F,x⟩\in \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)$$
11		df-br	$$⊢F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\leftrightarrow ⟨F,x⟩\in \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)$$
12	2	hlnvi	$$⊢U\in \mathrm{NrmCVec}$$
13		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
14	1	fveq2i	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
15	13 14	eqtr4i	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
16	15 4	imsxmet	$$⊢U\in \mathrm{NrmCVec}\to \mathrm{IndMet}\left(U\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)$$
17	5	mopntopon	$$⊢\mathrm{IndMet}\left(U\right)\in \mathrm{\infty Met}\left(\mathscr{H}\right)\to \mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)$$
18	12 16 17	mp2b	$$⊢\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)$$
19		lmcl	$$⊢\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\in \mathrm{TopOn}\left(\mathscr{H}\right)\wedge F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\right)\to x\in \mathscr{H}$$
20	18 19	mpan	$$⊢F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\to x\in \mathscr{H}$$
21	20	a1i	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\to x\in \mathscr{H}\right)$$
22	1 12 15 4 5	h2hlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$
23	22	breqi	$$⊢F\underset{v}{⇝}x\leftrightarrow F\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)x$$
24		brres	$$⊢x\in \mathrm{V}\to \left(F\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)x\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\right)\right)$$
25	24	elv	$$⊢F\left({\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)x\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\right)$$
26	23 25	bitri	$$⊢F\underset{v}{⇝}x\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\right)$$
27	26	baib	$$⊢F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\to \left(F\underset{v}{⇝}x\leftrightarrow F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\right)$$
28	27	adantl	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(F\underset{v}{⇝}x\leftrightarrow F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\right)$$
29	28	biimprd	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\to F\underset{v}{⇝}x\right)$$
30	21 29	jcad	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(F\underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)x\to \left(x\in \mathscr{H}\wedge F\underset{v}{⇝}x\right)\right)$$
31	11 30	biimtrrid	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(⟨F,x⟩\in \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\to \left(x\in \mathscr{H}\wedge F\underset{v}{⇝}x\right)\right)$$
32	31	eximdv	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(\exists x⟨F,x⟩\in \underset{t}{⇝}\left(\mathrm{MetOpen}\left(\mathrm{IndMet}\left(U\right)\right)\right)\to \exists x\left(x\in \mathscr{H}\wedge F\underset{v}{⇝}x\right)\right)$$
33	10 32	mpd	$$⊢\left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \exists x\left(x\in \mathscr{H}\wedge F\underset{v}{⇝}x\right)$$
34		elin	$$⊢F\in \left(\mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\leftrightarrow \left(F\in \mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)$$
35		df-rex	$$⊢\exists x\in \mathscr{H}F\underset{v}{⇝}x\leftrightarrow \exists x\left(x\in \mathscr{H}\wedge F\underset{v}{⇝}x\right)$$
36	33 34 35	3imtr4i	$$⊢F\in \left(\mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$
37	1 12 15 4	h2hcau	$$⊢\mathrm{Cauchy}=\mathrm{Cau}\left(\mathrm{IndMet}\left(U\right)\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)$$
38	36 37	eleq2s	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$