Theorem axhilex-zf

Description: Derive Axiom ax-hilex from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	axhil.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
Assertion	axhilex-zf	$$⊢\mathscr{H}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		axhil.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		axhil.2	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
3		df-hba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4	3	hlex	$$⊢\mathscr{H}\in \mathrm{V}$$